Алгебраические аксиомы без предусловий

Это сообщение посвящено стилям написания аксиом для алгебраических спецификаций. Согласно синтаксису аксиома имеет следующий вид: all var : type :- bool_expr [pre bool_expr] (предусловие необязательно). А алгебраическая аксиома имеет вид: all var : type :- expr is expr [pre bool_expr] , где оба expr - это функциональные термы, предусловие необязательно. Идея алгебраического способа записи свойств состоит в том, чтобы всякие хитрые кванторы и логические связи выразить только при помощи композиций операций системы. Предусловие - по сути тоже использует логическую связку (импликацию), поэтому можно было бы пытаться выражать аксиомы без нее, т.е. без предусловий. Посмотрим, во что это выливается, как при этом меняется способ формулирования аксиом.

Ближайшие мероприятия

29 декабря, 10:00-11:00, показ работ первой комиссии, аудитория 726, проставление зачетов студентам АСВК, АЯ и СП
29 декабря, 14:00, Михаил Игоревич Петровский проставляет зачеты студентам АСВК, кто не сможет прийти к 10, но успешно прошел комиссию
...где-то в десятых числах января..... вторая комиссия
19 января, 10:00, консультация к экзамену (готовьте вопросы по формулировкам задач экзамена!), аудитория П-14
21 января, 9:00-11:00, экзамен, аудитории П-5 и П-6. Распределение студентов по аудиториям планируется объявить на консультации.

Формальные спецификации в проблематике совместимости hardware/software

Одной из областей, где действительно на практике используются людьми и приносят свои плоды формальные спецификации, является стандартизация интерфейсов. Если вы пишете небольшой софт, в нем небольшое число компонентов, ваша группа разработчиков сидит в одной комнате и, даже возможно, с заказчиком можно "говорить и показывать" буквально в реальном времени, то разработка не встречает тех проблем, которые возникают во всех остальных случаях. Большие, разнесенные на расстоянии, коллективы, масса унаследованного кода, сторонние организации (возможно, не имеющие отношения к разработке кода), требующие соблюдения международных стандартов (например, они хотят продавать заказанный ими вам софт зарубежом) - это приводит к плохой управляемости проектом. Тяжело найти одного-двух человек, которые бы взвалили на себя ношу владения всей ситуацией и принятие ответственных решений по координации действий всех участников проекта. Спасением в этой ситуации, как ни странно, является более строгий подход к деятельности, в том числе с ведением всевозможной документации. В частности, документации об интерфейсах компонентов, которые разрабатываются независимо, но должны в конечном счете "заработать вместе". Сказать - одно, а сделать - другое: то, что документация как-то будет использоваться, практически очевидно, но как это сделать эффективно? Действительно, эффективное управление крупными проектами - это сложная вещь, на ВМК ее не преподают, у нас факультет не инженерный и не менеджерский. Но вот то, что касается документации по интерфейсам, возникающие при этом задачи, которые приводят к моделям программ и требований, это, на мой взгляд, может быть интересно. Какие возникают проблемы с описанием интерфейсов? Говоря двумя словами, очень немногие умеют описывать интерфейсы четко. Последствия этого, я думаю, очевидны из предыдущих предложений. Одним из способов четкого описания является составление формализованных (или даже формальных) описаний интерфейсов. Что это, как это - отношу вас к статье "Использование формальных методов для обеспечения соблюдения программных стандартов", написанную в том числе лекторами нашего курса. Советую ознакомиться. В этой статье, на мой взгляд, много и теоретического, и фактологического полезного материала по тому, как на практике используются формальные спецификации. Кому нравится видеть материал в более компактном виде, могу посоветовать слайды Виктора Кулямина под названием "Формализация интерфейсных стандартов на практике".

Где взять оффлайновую версию Dafny

Если у вас Windows, идете на http://boogie.codeplex.com, жмете справа большую зеленую кнопку Download и скачиваете последнюю ночную сборку (на rise4fun.com всё ещё старая версия, содержащая ряд багов, в том числе обнаруженных нами). Остается распаковать ее и запустить оттуда Dafny.exe. Не уверен, что на x86 заработает - у меня x64 и всё запутилось без проблем. Если ругается на отсутствие Z3, то скачиваете его с сайта этого солвера: http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html - и ставите. У меня на x64 всё запустилось сразу.

Комиссия может быть 2,5 часа

Комиссия 28 декабря начнется не в 10:00, как было объявлено ранее, а в 9:00. Время окончания и аудитория не изменились - 11:30 в П-8. Таким образом, длительность комиссии - 2,5 часа. Всем удачи!

Источники незамкнутости алгебраической спецификации

Среди различных характеристик алгебраических спецификаций можно выделить следующие три важные характеристики:

• полнота
• непротиворечивость
• замкнутость

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

Эти характеристики нужны при проведении валидации спецификации. Это сообщение посвящено тому, как проверять спецификацию на замкнутость.

Проставление зачетов 26 декабря

для студентов кафедры АСВК - после 11:00 в аудитории 753.

для студентов кафедры СП - с 9:30 до 10:30 в аудитории 726.

для студентов кафедры АЯ - с 10:30 до 13:00 в МЗ-4 (с досдачей RSL для тех, кому это актуально).

Показ работ основного зачета состоится

26 декабря в 9:30 в аудитории 726 (кафедра системного программирования).

Немного статистики

На потоке 127 человек. На первую попытку сдачи зачета пришел 81 студент. С первой попытки зачет сдал 31 студент (24% от общего числа на потоке, 38% пришедших на зачет). Все студенты, имеющие на данный момент автоматом "отлично" за экзамен, сдали зачет с первой попытки. Всем удачи на второй попытке сдачи зачета, aka основной зачет, 22 декабря.

Показ работ 21 декабря будет

в П-8а. Начало в 14:00.

Обновление дат мероприятий

21 декабря, 14:00, показ работ предварительного зачета, аудитория П-8а.


22 декабря, 10:00-11:30, зачет, аудитория П-5

26 декабря, 11:00-16:00, показ работ зачета

28 декабря, 10:00-11:30, комиссия, аудитория П-8
29 декабря, показ работ комиссии, проставление зачетов

Студенты АСВК могут проставить зачет при выполнении всех необходимых условий в аудитории 763 в рабочее время. Студенты СП могут проставить зачет при выполнении всех необходимых условий 22 или 26 декабря. Студенты АЯ могут проставить зачет при выполнении всех необходимых условий 22 декабря (возможно, 26го, но лучше уточнить у семинариста).

21 января, экзамен, аудитории П-5 и П-6

Как выписать decreases, если на разных итерациях убывают разные величины

Здесь будет очень кратко показано, как получать decreases в описанных в заголовке сообщения случаях. На самом деле предлагаемая здесь техника может быть применена и при решении задач на методы Флойда на зачете.

ACSL By Example

Для тех, кто хочет познакомиться с языком формальной спецификации программ на языке Си, ACSL, выпущено пособие под названием "ACSL By Example" (ссылка для скачивания). Написав спецификацию к программе на Си, можно воспользоваться инструментом Frama-C с плагином Jessie для автоматического получения условий верификации, корректности и завершимости в синтаксисе, пригодном для применения ряда автоматических пруверов (например, Alt-Ergo, CVC3, Z3, Simplify и т.п.) и интерактивных пруверов (например, PVS).

Экзамен пройдет 21 января

Планируются аудитории П-5 и П-6.

Всем, кто списывает задание по RSL

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

Крайний срок сдачи задания по RSL для 527-528 групп

Хотите проставить зачет 22 декабря (при успешно написанном Флойде 14 декабря), присылайте сделанное задание по RSL до 17 декабря.

Хотите проставить зачет 26 декабря (при успешно написанном Флойде 14 или 22 декабря), присылайте сделанное задание по RSL до 22 декабря.

В противном случае, у вас есть все шансы попасть на комиссию.

Если rsltc ругается на pre у аксиомы

Согласно синтаксису RSL, который поддерживает rsltc (RSL Type Checker), см. http://www.iist.unu.edu/www/newrh/III/3/1/docs/rsltc/user_guide/syntax.zip , pre у аксиомы можно писать только в том случае, если аксиома имеет вид all ... :- expr1 is expr2 . Если подкванторное выражение более сложное, надо либо его преобразовать к эквивалентности (это желательный способ избавления от этой проблемы), либо вместо pre записать импликацию (нежелательный способ решения этой проблемы).

Результаты второй контрольной работы групп 527 и 528

опубликованы .

Есть задачи для самоподготовки к зачету

См. на странице курса ссылку "Задачи по методам Флойда для подготовки к зачету (pdf, 70кБ)".

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

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

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

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

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

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

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

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

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

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

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

Крайне рекомендуется к прочтению всем, кто выполняет этап написания неявной спецификации в рамках практического задания по 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;
}