Даты зачетов

На лекции 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).