Этап написания неявной спецификации (корректность операций системы по отдельности с известным состоянием)

Это сообщение является продолжением сообщения "Для чего нужна часть курса ФСВП о спецификации" и посвящена имплицитным (неявным) спецификациям.

Крайне рекомендуется к прочтению всем, кто выполняет этап написания неявной спецификации в рамках практического задания по RSL.

Этап написания алгебраической спецификации (корректность систем "со скрытым состоянием")

Это сообщение является продолжением сообщения "Для чего нужна часть курса ФСВП о спецификации" и посвящена этапу написания алгебраической спецификации.

Крайне рекомендуется к прочтению всем, кто выполняет этот этап в рамках практического задания по RSL.

Для чего нужна часть курса ФСВП о спецификации

must read всем сомневающимся!

Возможно, не все понимают, зачем нужна первая часть нашего курса - та, в которой речь идет о формальной спецификации. Эта часть курса оправдана тем, что сейчас в практике программирования не редкостью является требование тщательной верификации кода (речь идет о верификации в широком смысле, тут и аналитическая верификация, и ручная экспертиза, и тестирование).

Конспекты бывшего спецкурса Д.Жукова по методам Флойда

На ВМК в своё время Дмитрий Жуков читал спецкурс, в первой части которого он рассказывал методы Флойда. Он подготовил конспекты по своему спецкурсу. Возможно, они вам пригодятся при подготовке к зачету и экзамену. [скачать pdf]

Лидеры после 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;
}