Computer science. Привет из ирландского университета

Город наводнен новыми интернациональными студентами.
Неожиданно много людей из США. К нам поселили парня из Луизианы по имени Майка (Micah) вместо Каролины, которую, как и всех бразильцев, выгнали из общежития после каникул по неизвестным причинам.
Еще есть люди из Южной Кореи. Я разговаривал с двумя. Оба играют за протосов. Ну и всякие новые немцы, австрийцы, голландцы.

В этом семестре у меня всего один предмет - Rigorous Software Process, на котором мы изучаем "доказательство программ".

(Начинается computer science, всем не интересующимся можно пропустить)

Скажем, есть метод (синтакс языка dafny)

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
requires 0 < y;
ensures less < x < more;
{
more := x + y;
less := x - y;
}

И для него заданы предусловия (preconditions) и постусловия (postconditions). Тут предусловие описывается в requires (y должно быть больше нуля). А постусловие - в ensures. Доказательство метода состоит в том, чтобы подтвердить или опровергнуть, что при соблюдении предусловий после выполнения метода постусловия станут истинны. Это происходит во время компиляции с помощью логики Хоара (если вдруг кому-то интересно, могу написать, как это конкретно делается).

Вот другой пример

int Abs(x: int)
ensures 0 ensures 0 x == y; // знак ==> - это импликация
{
if (x < 0)
{ return -x; }
else
{ return x; }
}

Все выглядит здорово и хорошо работает на мелких примерах, но стоит пойти глубже, и начинаются пляски с бубном.

Еще есть предмет под названием Program Comprehension, на который я хожу послушать лекции. Там мы делаем интересные штуки. В основном - статический и динамический анализ кода (на примере java). На первой лабе мы генерили UML диаграмму классов из готовых классов с помощью рефлексии. Потом считали сложность кода разными метриками (типа сколько веток алгоритма в методе). Потом строили граф вызовов - из какого метода вызываются какие другие методы. Потом делали динамический анализ кода средствами аспектно-ориентированного программирования. Это все интересно, и довольно просто. Есть хорошие библиотеки для анализа байткода.

Еще в этом семестре у нас есть криптография, но я на нее не ходил. Говорят, там сплошная математика.

(Дальше нормальный текст, можно читать)

Все остальные дни по идее я должен работать над моим дипломным проектом, который будет на тему создания Domain Specific Language.

Нам даже выделили для этого отдельную лабораторию с компами (!)



Вот это моя одногруппница Агастья из Индонезии. Практически живет в лаборатории. Ее проект - определять по данным акселерометра телефона, что человек упал, и отправлять сообщение родственникам. Секция дзюдо дала ей мат для тестирования.

А вот это моя кабинка.


Всем сказали работать с git, сделали каждому репозиторий. Всю работу нужно будет отправлять на сервер по мере выполнения.

А еще в библиотеке я нашел медиа-раздел. Тут куча пластинок, кассет, дисков - музыка, аудиокниги, фильмы.

Экзамены, предметы, оценки в National University of Ireland Maynooth, Андрей Ковалёв

Добрая печальная жизнь ирландских китов, Андрей Ковалёв, 26-05-2014