Рубрика: Новости

Пересдача

Пересдача состоится 3 сентября в 12:15 в аудитории 727. Формат пересдачи такой же, как и экзамена. Семестровые баллы обнуляются. Оценка будет выставлена по итогам решения упражнений и ответов на вопросы по ним.

Экзамен

14 июня состоится экзамен. Он пройдет в аудитории 526-Б и начнется в 9:00 (информация про аудитории 72 и 73 устарела). Экзамен длится 120 минут. Экзамен письменный. Будут предложены задачи и упражнения по всему курсу. Можно пользоваться любыми письменными и напечатанными материалами. Нельзя пользоваться электронной техникой. Показ работ и выставление оценок пройдут в этот же день.

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

В рамках практического задания нужно написать формальную спецификацию требований к некоторой структуре данных и операциях над нею (этап 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 марта.