Домашние задания — Формальные методы разработки программ

Домашняя работа №4 по языку Си

Пусть есть некоторый тип данных Value. Реализуется стек (LIFO) из элементов этого типа.

Для этого определяются следующие глобальные переменные:
Value *stackItems;
int stackCapacity;

stackItems — это массив для хранения элементов стека. Переменная stackCapacity хранит размер этого массива. Оно же равно предельному числу переменных типа Value, которые можно поместить в стек.

Функция int stackInit(int capacity); предназначена для создания пустого стека с максимальным количеством элементов capacity. Если это удается, функция возвращает 0. Иначе функция возвращает ненулевой код ошибки. Далее размер массива не меняется.

Функция int stackPush(Value *value); предназначена для добавления *value на вершину стека. Если это удается, функция возвращает 0. Иначе функция возвращает ненулевой код ошибки.

Функция int stackPop(Value *value); предназначена для извлечения элемента с вершины стека и записи его по указателю value. Если это удается, функция возвращает 0. Иначе функция возвращает ненулевой код ошибки.

Других функций, работающих с этими переменными, нет.

Исходный текст заголовочного файла с объявлениями переменных и функций можно скачать по этой ссылке. Вам нужно дополнить его спецификациями переменных и функций, отражающими все вышеописанные требования (и только их). Готовый файл отправляйте на почту до 12:00 23 апреля.

Домашняя работа №3 по языку Си

Пусть есть глобальные переменные
int *maxValues;
int maxValuesCount;

Пусть есть функция
void action(int v);

Переменная maxValuesCount предназначена для хранения размера массива maxValues. Массив maxValues предназначен для хранения maxValuesCount максимальных по значению различных аргументов функции action в порядке убывания. Функция action не теряет аргументы, а лишь дополняет массив maxValues значением своего аргумента, если его там не было. Других функций, изменяющих указанные глобальные переменные, нет.

Написать спецификации, отражающие все вышеописанные требования (и только их!).

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

Задание нужно сделать и отправить на почту до 12:00 9 апреля.

Домашняя работа №2 по языку Си

В задании речь идет о модуле для работы с банковским счетом. В модуль включены две функции — deposit и withdraw, которые работают с глобальной переменной account. Предполагайте, что модуль может быть расширен, то есть может быть написан модуль с дополнительными функциями, включающий этот модуль, работающий с той же глобальной переменной account. Это расширение не должно нарушать допустимое множество значений этой переменной.

Переменная account обозначает количество денег на счете. Оно не может быть отрицательным и должно укладываться в тип.

Функция deposit предназначена для того, чтобы положить некоторую положительную сумму денег на счет. Если это можно сделать, функция должна увеличивать значение переменной account на эту сумму денег и возвращать число 0, других действий эта функция не должна делать. Если положить указанную сумму нельзя, функция должна возвращать число 1 и не делать никаких других действий.

Функция withdraw предназначена для того, чтобы снять некоторую положительную сумму денег со счета. Если это можно сделать, функция должна уменьшать значение переменной account на эту сумму денег и возвращать число 0, других действий эта функция не должна делать. Если снять указанную сумму нельзя, функция должна возвращать число 1 и не делать никаких других действий.

Заголовочный файл модуля можно скачать по этой ссылке.

Задание: 1) дополнить заголовочный файл спецификацией модуля; 2) написать реализацию модуля и доказать при помощи Frama-C, что реализация удовлетворяет спецификации; 3) прислать на почту архив с директорией, в которой есть заголовочный файл со спецификацией, реализация и директория .jessie с доказательством.

Задание должно быть выполнено до 12:00 2 апреля.

Домашняя работа №1 по языку Си

В домашней работе два задания. Второе задание выполняется только после успешного выполнения первого задания.

1) Напишите заголовочный файл *.h c формальной спецификацией на ACSL функции, вычисляющей ближайшее снизу целое число к квадратному корню данного целого числа. Файл должен приниматься Frama-c + Jessie. Пришлите его на почту .

2) Докажите полную корректность выданной преподавателем реализации этой функции относительно вашей спецификации при помощи инструментов Frama-c + Jessie. На почту нужно прислать zip-архив целиком директории, в которой находится файл *.h со спецификацией, файл *.c с реализацией, включающий заголовочный файл при помощи #include, и директория *.jessie, созданная инструментом. Для этого после успешного доказательства всех условий верификации сохраните сессию (File > Save session). Проверка будет выполняться открытием этой сессии и нажатием кнопки Replay.

Всё задание должно быть выполнено до 12:00 26 марта.

Домашняя работа по методам Флойда с частичными функциями

Докажите, что эта блок-схема (картинка) полностью корректна относительно этой спецификации при помощи методов Флойда. Решение присылайте на почту до 12:00 17 марта в виде двух файлов: файла *.py с индуктивными утверждениями и оценочными функциями в формате PyFloyd и 2 файла *.prf с PVS доказательством истинности условий из метода индуктивных утверждений и метода фундированных множеств. Индуктивные утверждения в файле *.py должны годиться и для доказательства частичной корректности, и для доказательства завершаемости.

Обратите внимание, что команда PVS (grind) не применяет аксиомы и леммы. При необходимости можно добавить аксиому или лемму в список антецедентов при помощи команды (lemma) и продолжить доказательство при помощи (grind).

Для поддержки частичных функций обновите инструмент PyFloyd.

Домашняя работа по методу фундированных множеств

Докажите, что эта блок-схема (картинка) завершается на этом предусловии при помощи метода фундированных множеств. Решение присылайте на почту до 12:00 5 марта в виде двух файлов: файла *.py с индуктивными утверждениями и оценочными функциями в формате PyFloyd и файла *.prf с PVS доказательством истинности условий верификации.

Обратите внимание, что инструмент PyFloyd поддерживает (пока) единственное фундированное множество: неотрицательные целые числа и арифметическое сравнение «меньше», а множеством значений всех оценочных функций является множество всех целых чисел.

Домашняя работа по методу индуктивных утверждений Флойда

Докажите, что эта блок-схема (картинка) частично корректна относительно этой спецификации при помощи метода индуктивных утверждений Флойда. Решение присылайте на почту до 12:00 26 февраля в виде двух файлов: файла *.py с индуктивными утверждениями в формате PyFloyd и файла *.prf с PVS доказательством истинности условий верификации.

Рубрика: Домашние задания