Лидеры после 1 декабря

(54) Кошелев Владимир, 527 группа
(47) Куликов Василий, 524 группа
(34) Меркулов Алексей, 527 группа
(30) Вдовин Павел, 522 группа
(28) Иванкова Анна, 524 группа
(28) Кадысев Михаил, 527 группа
(27) Куприк Илья, 528 группа
(27) Джумаев Станислав, 525 группа
(26) Боловинцева Олеся, 525 группа
(25) Клычков Денис, 524 группа

ghost методы в Dafny могут изменять heap

Например, эта программа не доказывается по этой причине: http://rise4fun.com/Dafny/wp1 (объяснение см. в предыдущем посте). Чтобы указать, что ghost метод на самом деле не меняет память, надо его обрамить так:

ghost var cc := a[..];
call the ghost method
assert cc == a[..];

Результат: http://rise4fun.com/Dafny/zNyn .

Если Dafny не верит в неизменность массива

Пусть есть метод, который переставляет два первых элемента некоторого массива:

method Main(a : array<int>)
   requires a != null;
   requires a.Length > 1;
   modifies a;
{
     var t := a[0]; a[0] := a[1]; a[1] := t;
}

Даты зачетов

На лекции 14 декабря будет проведен "предварительный" зачет по курсу. Длительность - два академических часа. Вам будет предложено решить задачу на Флойда за два академических часа. Успешно справившиеся с этой задачей, не приходят на основной зачет - им Флойд уже будет зачтен.

22 декабря в 10:00 будет проведен сам зачет по курсу у всего потока сразу. Длительность - два академических часа.

На 28 декабря планируется комиссия по курсу. Вторая комиссия, как и обычно, проводится уже в январе.

Функция multiset в Dafny

Еще одна недокументированная возможность Dafny - функция multiset. Она принимает один аргумент - seq - и возвращает "мультимножество", в котором есть ровно те же элементы, что и в seq'е, но без какого-либо порядка. Ее можно использовать для спецификации свойств перестановок элементов seq'а.

Результаты 524 и 525 групп

В таблице с текущими баллами опубликованы баллы за вторую контрольную и за семинары в группах 524 и 525.

Еще про ghost в Dafny

В tutorial'ах по Dafny написано, что ghost можно объявить локальную переменную, поле класса, метод класса. Но, оказывается, можно объявить и возвращаемое значение ghost. Это помогает избежать ненужных кванторов существования и повысить эффективность автоматического доказательства. Каким же образом. Представим, что пишется метод, вычисляющий максимум в непустом массиве. В его постусловии будет записано, что существует такое число в границах индексов массива, что возвращаемый максимум является элементом массива с индексом по этому числу. Но ведь в коде метода и так вычисляется этот индекс, а в постусловии по сути лишний раз записываются свойства этого индекса. Двойную работу можно попытаться снять, объявив этот индекс ghost возвращаемым значением! И тогда постусловие станет проще: из него уйдет квантор существования: