Домашняя работа №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 необходима реализация для вычисления регионов).

Тип данных Stack описывает последовательность целых чисел. Поле buffer означает указатель на начало массива, размещаемого в динамической памяти, в котором хранится последовательность чисел. Последовательность чисел хранится в массиве, начиная с его начала без пропусков. Поле capacity не должно быть отрицательным или равным нулю и не может быть больше размера массива buffer. Поле count означает количество элементов последовательности целых чисел, оно не может превышать поля capacity.

Операция Stack__init предназначена для инициализации структуры данных Stack пустой последовательностью чисел. Функцию можно вызывать только для указателей-параметров, указывающих на выделенную область памяти.

Операция Stack__final предназначена для удаления ресурсов, задействованных для структуры данных Stack.

Операция Stack__push(s, v) предназначена для добавления в конец последовательности чисел s числа v.

Операция Stack__pop(s, v) предназначена для удаления из последовательности чисел s последнего добавленного элемента и записи его в переменную v.

Все функции, кроме Stack__init, можно вызывать только для указателей на корректный Stack. Возврат функциями числа 0 означает, что они успешно выполнили свою задачу. Ничего, кроме описанного выше, функции не должны делать. Функции могут менять содержимое структуры, если это не отражается на содержащейся в ней последовательности чисел.