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

Это сообщение посвящено стилям написания аксиом для алгебраических спецификаций. Согласно синтаксису аксиома имеет следующий вид: 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;
}

Даты зачетов

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

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

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

Функция multiset в Dafny

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

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

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

Еще про ghost в Dafny

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

Почему Dafny трудно доказывать свойства с кванторами существования

Попросим доказать очевидное:

method m1()
{
    assert exists y :: 0 <= y <= 100;
}

и получим: assertion violation ! Но почему ?

Выдача дополнительных практических заданий завершена

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

Пример выполнения практического задания по RAISE : этап первый (часть первая)

Постановка задачи.
Требуется реализовать программу Geolocator (это задание предлагалась в 2009 году). Программа предназначена для мобильного устройства. Она отображает карту некоторой местности и то, что на ней находится. Программа должна уметь:
- сохранять указанные пользователем описания мест на карте ("Здесь живу я", "Тут мой любимый Университет" и т.п.).
- показывать места в части карты, указанной пользователем.
- при показе должны учитываться как указанные пользователем, так и подгружаемые с публичных серверов описания мест.
- хочется иметь опцию, публиковать ли свое описание на публичном сервере.

Делаем анализ предметной области.
Выделяем понятия нашей системы: карта, видимая часть карты, место, описание места.

Пытаемся увидеть проблемы:

Автоматически подгружать "всё, что угодно" на карте не получится. Во-первых, много трафика, во-вторых, всё равно всё, возможно, будет и не отобразить. Т.е. видим проблему: возможен огромный объем данных, а раз он огромный, то его нельзя будет отобразить. Думаем, как обычно решают эту проблему => Вводят категории мест ("Личное", "Развлечения", "Учеба", "Работа" и т.п.), на карте отображаются только места из определенных категорий. Ок, теперь у нас все появились категории. Но это категории чего? Мест? Описаний мест? И не то,  и не другое (описание - это текст, у текста не может быть категории "Личное", "Развлечения"; месьл - это адрес, по одному адресу может быть как то, что относится к желаемым категориям, так и то, что не относится). Так всё же, категории чего у нас есть? Получается, что категории некоторого "объектов". Объект располагается в месте, для объекта задается описание. Думаем об арности: может ли быть у одного объекта много мест? Может ли быть у одного места много объектов? Может ли быть у одного объекта много описаний? Может ли один объект относиться к нескольким категориям?

А откуда программа наша узнает, какие вообще есть категории? Значит, нужно уметь еще и подгружать категории. Запомним это! Если описаний много, все ли нас интересуют? Явно не все, т.е. есть некие "полезные", а есть "неполезные" описания. А как выбирать полезные описания? Как задать, что такое "выбрать полезные описания"? Это проблема, ведь понятие "полезного описания" неформальное! В неформальном описании требований можно написать "программа должна показывать только полезные описания мест", а в формальной спецификации так писать нельзя, нужно дать четкое определение, какие описания будут считаться полезными. Пока мы этого не сделали. Так всё же, как понять, какие описания полезные?

Как показывать места, у которых несколько объектов? Просто ставить "точку" с описанием нельзя (всё сольется в непонятную "кашу"), надо четко подумать, как показывать информацию, чтобы не получилось мешанины. Итак, еще одна проблема, как программа должна показывать такие места?

Думаем дальше, очевидно, что карта большая. Значит, вся не влезет на экран. Как быть? Как обычно решают эту проблему? Вводят масштабирование. Значит, у нас будет масштабирование. Можно приближать часть карты, удаляться, передвигаться (кстати, это новые возможности программы, о которых не было сказано в постановке задания - это правильно, что появляются такие новые возможности? или, если их нет в постановке задания, то и появляться они не должны?). Ок, но представим, что мы выбрали некий масштаб, сказали программе, "покажи все места с объектами такой-то категории на этом участке карты" (потому что нам эта категория интересна, например, "Магазины модной одежды"), и, о, ужас, программа завалила весь показываемый участок карты символами мест так, что невозможно разобрать ни одно из них! Значит, надо уметь выбирать, "фильтровать", показываемые объекты, даже в пределах выбранного участка карты и категории объектов. Т.е. надо выбирать "нужные объекты", а что такое, эти "нужные объекты"? Опять попали в область неформального. Итак, проблема: как дать определение "нужного объекта на карте" ?

Но и это еще не всё. Пользователь куда-то "тыкает" в карту, карта находится не на мелком масштабе и в результате пользователь тыкает не в то место, где реально располагается объект. Скажем, видит всю карту Москвы, тыкает "приблизительно в районе Ленинских гор", чтобы указать, что он тут учится и тут находится факультет ВМК :) (а на самом деле метка может попасть куда-нибудь, например, в здание экономического факультета) Его метка попадает на публичный сервер. А через некоторое время некий абитуриент, который хочет поступать на ВМК, считывает с публичного сервера метку - и, о ужас, приходит подавать документы на экономический факультет, и этот абитуриент для нас потерян! Итак, проблема неточной постановки мест на карте - это действительно проблема для нашей программы или нет?

Раз речь зашла про публичный сервер, куда многие могут засылать места, объекты и их описания, то, очевидно, этот сервер быстро превратится в "помойку". Там будет не просто очень много информации, а там будет и просто ложная информация. Итак, очередная проблема: поддержание корректности данных на публичном сервере. Ее решение - это задача нашей программы? Или так, может ли наша программа хотя бы частично помочь серверу в определении заведома плохой информации, которую пытаются туда заслать?

Мы сформулировали уже очень много вопросов, хотя, казалось бы, всё начиналось лишь с одного абзаца текста с описанием желаемой системы. Заказчик ее видел достаточно просто, но мы должны взглянуть на систему более пристально, чтобы в результате получился как можно более лучший продукт.


(продолжение следует; крайне приветствуются комментарии!)

Дедлайн по RAISE для 527 и 528 групп

Проставление зачета по курсу в срок студентам 527 и 528 групп не гарантируется, если сделанное практическое задание по RAISE будет прислано после 10 декабря 2011 года. Результат своей работы присылайте на почту kornevgen@cmc.msu.ru . Не забудьте к неявной и явной спецификациям написать обоснование выбора структур данных и алгоритмов (оно должно исходить из нефункциональных требований!!!).

Работа с предметной областью при выполнении задания по RSLцификация)

Здесь будет дан ряд пожеланий к тому, как надо выполнять практическое задание по RAISE, для чего оно нужно. Здесь речь пойдет в основном про описание логики работы программной системой, с которой Вы работаете по заданию, т.е. про написание алгебраической спецификации.

Представьте, что Вы разработчик, Вам дают ТЗ, Вы должны с ним ознакомиться и реализовать то, что там написано. Представим ситуацию, Вы прочли задание и говорите: "Мне всё ясно". "Отлично", говорит заказчик, и Вы уходите работать. Когда всё готово, приходит заказчик, смотрит, что получилось, "щупает" его в разных местах - и, о, он высказывает кучу замечаний (он хотел по-другому, он подразумевал другое) ! Неужели получилась плохая работа? Или вот другой случай. Вы уходите разрабатывать систему и через некоторое время выясняется, что в ТЗ одно требование противоречит другому или в ТЗ мелькают слова "интуитивно понятные", но лишь обманчиво понятные, а на деле - совершенно непонятные! И приходится останавливать работу или, что еще хуже, приходить к мысли, что сделанное ранее надо "выкидывать в мусор", оно не соответствует реальному пониманию технического задания.

Не знаю, как Вам, а вообще-то так вести разработку неправильно. Затратно и неприятно. Было бы здорово, если основную массу дефектов в ТЗ кто-то обнаружил и исправил заранее (на самом деле, не исправил, а обнаружил, задал вопрос заказчику и на основе него исправил ТЗ, только вот, что спрашивать?). В практическом задании по RAISE Вам предлагается (в частности) выполнить функции такого "Робин Гуда". Вы должны сделать всё, чтобы разработка по точно сформулированному Вами заданию прошла без возражений к логике работы системы. Т.е. точно сформулировать требования, постановку задачи, увидеть все скрытые ранее логические зависимости понятий (эти зависимости должны быть отслежены в реализации). Требования удобно писать в виде алгебраической спецификации, потому что Вы просто синтаксически не сможете выразить какие-либо реализационные домыслы, не относящиеся к логике работы системы.

Итак, надо подумать и выразить в спецификации следующие моменты:

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

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

Появилась таблица с текущими результатами

https://docs.google.com/spreadsheet/pub?hl=ru&hl=ru&key=0AoN5iJE0CvIadFlhUzZMZjRyZV9oUGVob2tvdWhpWFE&single=true&gid=0&output=html

Окончание выдачи доп.практических заданий

20 ноября прекращается выдача дополнительных практических заданий (по Dafny и PVS).

Информация об экзамене и зачете

На странице курса появилась информация о том, как будет проводиться зачет, как будет проводиться экзамен, какая система получения оценки по курсу, какие в курсе есть практические задания: http://sp.cmc.msu.ru/courses/fmsp/fsvp2011.pdf .