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

В рамках практического задания нужно написать формальную спецификацию требований к некоторой структуре данных и операциях над нею (этап 1) и доказать полную корректность одной из реализаций операций относительно их спецификаций (этап 2). Язык реализации — Си, язык спецификации — ACSL, инструменты доказательства — frama-c+jessie2+why3+солверы.

Этапы задания выполняются последовательно. Реализация для выполнения этапа 2 выдается преподавателем после успешной сдачи этапа 1. Этап 1 сдается только очно, этап 2 может сдаваться заочно. Дни для сдачи этапа 1: 11 апреля, 18 апреля, 25 апреля, 16 мая, с 13:50 до последнего сдающего, но не позднее 17:20. При отсутствии желающих сдавать до 14:05 сдача в данный день прекращается. Преподаватели оценивают правильность выполнения этапа и могут не давать комментариев о месте ошибки в исходных текстах спецификаций. Можно пытаться сдавать несколько раз. Этап 1 считается выполненным только целиком и не оценивается частично.

Текст, общий для всех вариантов задания, и файлы находятся по этой ссылке. Для получения варианта нужно отправить письмо на почту

Контрольная работа №2

На лекции 11 апреля состоится контрольная работа по спецификации. В контрольной работе будет два задания. В первом задании нужно будет написать спецификацию для типа данных и операций над ним (как в домашней работе №8). Во втором задании будет дана реализация функции и спецификация для нее и нужно будет вставить аннотации в текст функции, чтобы связка инструментов frama-c+jessie2+why3+солверы доказала полную корректность этой реализации относительно ее спецификации. В реализации будут использоваться указатели, при верификации надо учитывать разделение по регионам.

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

Домашняя работа №8

В архиве по этой ссылке находятся исходные файлы для выполнения задания:

  • заголовочный файл stack.h с определением структуры данных Stack и заголовками функций Stack__init, Stack__final, Stack__push и Stack__pop
  • файлы с реализациями этих функций: dummy_stack.c, true_stack.c, magic_stack, realloc_stack
  • файл main.c с функцией main().

В заголовочном файле на языке ACSL напишите спецификацию структуры данных Stack и всех операций над ним согласно приведенным требованиям. При помощи связки инструментов frama-c+jessie2+why3 докажите, что все реализации этих операций полностью корректны относительно их спецификаций. При помощи связки инструментов frama-c+jessie2+why3 докажите полную корректность функции main(). При необходимости вставляйте дополнительные аннотации в текст функций. Не меняйте спецификацию функций в файлах с реализациями. Далее перечислены требования к этому типу данных.

Это задание является подготовкой к контрольной работе №2. Крайне рекомендую выполнить эту домашнюю работу до контрольной работы. Архив с дополненными файлами и сессиями доказательства присылайте на почту до 23:59 12 апреля. Полную корректность функции main() необходимо доказывать совместно с каждой из реализаций операций (это следствие того, что инструменту Jessie2 необходима реализация для вычисления регионов).

Читать далее «Домашняя работа №8»

Срок сдачи домашней работы №7

Срок сдачи домашней работы №7 продлевается до 23:59 3 апреля. Свои вопросы и решения присылайте на почту

28 марта ноутбуки с Frama-C могут быть полезны

Лекция и семинар 28 марта будут посвящены использованию нашей связки инструментов frama-c+jessie2+why3 для доказательства полной корректности. Будет много живых демонстраций доказательства. Очень рекомендую взять с собой ноутбук установленными инструментами, чтобы можно было повторять за мной действия и сразу задавать вопросы.

Домашняя работа №7

Задача 1. Напишите теорию Why3 таблиц аллоцированных блоков динамической памяти. В этой теории введите типы для таблицы и указателя, предикатного символа valid для проверки корректности разыменования указателя и все остальное вместе с аксиомами для решения последующих задач. Можно предположить, что все блоки имеют одинаковый размер (не массивы) и нет указателей внутрь блока. Не забудьте проверить непротиворечивость своей теории!

Задача 2. При помощи этой теории напишите теорию Why3 с предусловиями и постусловиями Си-функций malloc и free. Можно предположить неограниченность памяти. Можно предположить, что эти Си-функции используется для работы только с блоками того же размера, что и в теории из задания 1.

Задача 3. Напишите блок-схему, полностью корректную относительно указанной ниже спецификации. Блок-схема должна быть составлена по некоторой Си-функции. Функциональные и предикатные символы из задания 1 не могут использоваться в коде Си-функции (они не являются Си-функциями).

/*@
    requires valid(p, pre_alloc_table);
    ensures !valid(p, post_alloc_table) && valid(\result, post_alloc_table);
*/
char *foo(char *p);

Задание 4. Напишите теорию Why3 с доказательством полной корректности блок-схемы из задания 3 относительно указанной у нее спецификации и проведите доказательство. Укажите в комментарии блок-схему и Си-функцию из задания 3.

Решение (теории с комментариями и сессию доказательства) пришлите на почту до 23:59 30 марта.

Домашняя работа №6

Задача 1. Дана блок-схема над 1 входной переменной, 1 промежуточной переменной и 1 выходной переменной. Домены всех переменных — множество всех целых чисел. Сигнатура \(mc91\) имеет домены аргументов и результатов — множества всех целых чисел. При помощи методов Флойда докажите полную корректность этой блок-схемы относительно спецификации \(\varphi(x) \equiv T\), \(\psi(x, z) \equiv (x \geq 101 \Rightarrow z = x — 10) \land (x < 101 \Rightarrow  z = 91)\), если сигнатуре \(mc91\) сопоставлена данная блок-схема.

Решение (теорию со всем необходимым, а также сессию доказательства) присылайте на почту до 23:59 22 марта. Требования к оформлению решения те же, что и в прошлой домашней работе.

Контрольная работа по методам Флойда

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

Домашняя работа №5

Задача 1. Дана блок-схема над 2 входными переменными, 2 промежуточными переменными и 1 выходной переменной (алгоритм Евклида). Домены всех переменных — целочисленные. При помощи методов Флойда докажите полную корректность этой блок-схемы относительно спецификации \(\varphi(x_1,~x_2) \equiv x_1 > 0 \land x_2 > 0\), \(\psi(x_1, x_2, z_1) \equiv (z_1 = gcd(x_1, x_2))\). Функциональному символу \(gcd\) сопоставлена функция, вычисляющая наибольший общий делитель двух чисел. Это определяется в этой теории Why3.

Решение (теорию с индуктивными утверждениями, оценочными функциями, условиями (в виде целей) и комментариями, а также сессию доказательства) присылайте на почту до 23:59 15 марта. Требования к оформлению решения те же, что и в прошлой домашней работе. В вашей теории нужно импортировать теорию gcd по ссылке выше. Солверы сами смогут использовать аксиомы, определяющие символ gcd, из этой теории.