Практическое задание по Dafny

Постановка задания

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

Для решения задачи вам выдаётся готовый набор классов и методов, моделирующих стандартную библиотеку языка Си.

Вам необходимо переписать данный исходный текст на язык Dafny (в соответствии с указаниями, приведенными ниже). После чего снабдив его полной спецификацией до такого состояния, чтобы инструмент Dafny автоматически доказывал его корректность. По окончании работы необходимо прислать Денису Буздалову на адрес public@buzden.ru один файл с расширением dfy, содержащий решение. Присланный файл не должен содержать кода, выданного преподавателями. Кроме того, присланный код должен успешно проходить проверку инструментом Dafny (за исключением, postcondition might not hold для 1 этапа). Для 2 этапа присланный код не должен содержать синтаксических ошибок (другие сообщения верификатора допускаются на этом этапе). В частности, на этапе 2 не обязательно писать инварианты.

Ход выполнения задания

  1. Сформулировать заголовок метода и его программный контракт на языке Dafny для главной подпрограммы. При этом следует использовать классы языка Dafny, выданные преподавателями,  для указателей, массивов и прочих сущностей языка Си. Программный контракт должен полностью описывать задачу, которую должна решать главная подпрограмма.
  2. Аккуратно переписать тело главной подпрограммы и остальные подпрограммы с языка Си на язык Dafny, используя выданные преподавателями классы. Классы находятся в репозитории на github.com: https://github.com/buzden/dafny-c-lib. В своём решении вы можете использовать любые классы, методы и функции, которые находятся в этом репозитории.
  3. Провести верификацию полученной реализации на языке Dafny средствами инструмента Dafny. При этом, возможно, придется добавить в код спецификационные конструкции (например, инварианты). Инструмент Dafny можно использовать как в онлайн-версии на http://rise4fun.com/dafny (правда, при этом придется вставлять туда исходные тексты с dafny-c-lib), так и в оффлайн-версии (её можно скачать с http://boogie.codeplex.com и вызывать из командной строки, передавая в качестве параметров все файлы с необходимыми классами, методами и функциями).
  4. Если в результате верификации обнаружится, что выданный код не является корректным, необходимо сообщить об этом преподавателям, предложить исправление, внести его и продолжать верификацию.

Рекомендуется использовать материалы по Dafny, размещенные на странице курса ФСВП (http://sp.cmc.msu.ru/courses/fmsp).

Подсчёт очков за задание

За задание можно получить до 20 баллов. Этапы 1 и 2 оцениваются в 4 балла каждое (при их выполнении в срок), этапы 3 и 4 оцениваются в 12 баллов вместе.

Сроки выполнения задания

06:00 (мск время) 7 ноября - дедлайн по этапу 1

06:00 (мск время) 13 ноября - дедлайн по этапу 2. Этот этап рассматривается преподавателями вне зависимости от этапа 1. Поэтому можно присылать решения этапа 2, не ожидая ответа преподавателей по этапу 1.

06:00 (мск время) 10 декабря - дедлайн по этапам 3 и 4 (совместно). Эти этапы рассматриваются преподавателями только при сданных первых двух этапах.

Модель памяти

Не любая программа на языке Си может быть легко перенесена на язык Dafny. Проблема в том, что у этих языков принципиально различные модели памяти. Тем не менее, это не мешает проводить верификацию для части программ на Си, использующие память согласно семантике языка Dafny. Язык Dafny предполагает, что динамическая память состоит из объектов и массивов. Каждый массив занимает свою непрерывную часть памяти и каждый объект занимает свою непрерывную область памяти, причем для разных объектов/массивов эти области не пересекаются. Массивы являются типизированными. В языке Dafny отсутствуют “указатели”, как они понимаются в языке Си. Вместо этого в Dafny (как и в Java, кстати) все переменные типа объекта и массива являются ссылками. Ссылки можно присваивать друг другу, можно присваивать и читать значения по ссылке.

Ваши программы на языке Dafny будут использовать объекты и массивы Dafny (т.е. модель памяти Dafny), но сами объекты и массивы будут представлять сущности языка Си. У этих объектов и массивов будут определены свойства, гарантирующие выполнение функциональности, подобной модели памяти языка Си. Итак, модель памяти типизированная, с контролем границ.

Надо заметить, что несмотря на большие различия между моделью памяти языка Си и языка Dafny, данное практическое задание можно выполнить без явного моделирования одной модели памяти в другой, что существенно упрощает как верификацию (т.е. обоснование корректности реализации на языке Си), так и спецификацию поведения программы на Dafny. Тем не менее, предлагаемый в данном практическом задании способ верификации программ на языке Си не является единственным и существует достаточно много разных инструментов и языков спецификации и верификации программ на языке Си (например, ACSL и Frama-C, VCC и другие).

Dafny-c-lib

Для уменьшения трудоемкости вашей работы преподаватели реализовали ряд классов, методов и функций на языке Dafny, моделирующие ряд сущностей и функций языка Си и стандартной библиотеки языка Си. Определения этих классов размещены в репозитории на github.com (https://github.com/buzden/dafny-c-lib). В частности, там есть класс Pointer<T>, моделирующий указатели языка Си, метод malloc, моделирующий функцию стандартной библиотеки языка Си malloc, и т.п.

Каждый класс, метод или функция, размещенные в dafny-c-lib, снабжены подробной документацией. Внимательно ознакомьтесь с этой документацией. Кроме того, в этих классах записаны ограничения на ваше решение (в частности, не разрешается присваивать друг другу переменные типа Pointer<T> для моделирования присваивания указателей языка Си). Все эти ограничения являются необходимыми.

Дополнительно следует проследить о том, что:

1) зачастую требуется, что вся выделенная (временная) динамическая память должна быть освобождена; это свойство следует записать следующим образом:

allowedMemory().blocks == old(allowedMemory().blocks) + { … }

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

Все возникшие вопросы по dafny-c-lib задавайте Денису Буздалову (public@buzden.ru).

Пример выполнения

Рассмотрим выполнение задания на примере функции memcpy. Её исходный текст на языке Си такой:

void *memcpy(void *dest, const void *src, size_t n)

{

        size_t curr = 0;

        while (curr < n) {

                dest[curr] = src[curr];

                cur++;

        }

        return dest;

}

Читаем спецификацию этой функции:

The memcpy() function copies n bytes from memory area src to memory area dest.        

The memory areas must not overlap. The memcpy() function returns a pointer to dest.

Согласно этой спецификации были написаны предусловия и постусловия для memcpy на Dafny. Их можно посмотреть в dafny-c-lib/system.dfy.

Обратите внимание на modifies у метода memcpy : src объявлен как const void *, т.е. указатель на неизменяемую память, поэтому у метода memcpy отсутствует modifies src.memory; а раз dest объявлен как void * (как указатель на изменяемую память), то у метода memcpy присутствует modifies dest.memory;