Задача 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 марта.