Задание по алгебраической спецификации: основные дефекты

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

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

Основные дефекты - это

• отсутствие достаточно представительного набора функциональных свойств;
• неполнота (эффект цепочки функций описывается не на всех данных, на которых его можно описать);
• (как следствие предыдущих дефектов) игнорирование частичности функции (функция объявляется как тотальная, хотя она таковой не является, не должно быть возможности ее применить ко всем входным значениям, подходящим под типы).

Алгебраические спецификации в Dafny

Dafny позволяет определять абстрактные типы данных и использовать их в функциях и "теоремах". Эти средства явно намекают на возможность описания функциональности программных систем в алгебраической манере. Посмотрим, как это происходит и что это нам дает.

Предварительный зачет будет в П-12

Ввиду проведения некой конференции на факультете, наш предварительный зачет пройдет не в П-8 + П-8а, а в П-12.

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

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

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

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

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

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

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

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

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

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

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