Домашняя работа №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 марта.

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Этот сайт использует Akismet для борьбы со спамом. Узнайте как обрабатываются ваши данные комментариев.