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

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

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

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

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

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

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

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

Контрольная работа по методам Флойда

На семинаре 15 марта будет проведена контрольная работа по методам Флойда. Длительность контрольной — 1,5 часа. За это время нужно будет доказать полную корректность некоторой блок-схемы относительно некоторой спецификации при помощи методов Флойда. Можно пользоваться любыми письменными материалами и книгами. Нельзя пользоваться электронными устройствами.

Еще одно пособие

Вашему вниманию предлагается пособие Камкина Александра Сергеевича «Введение в формальные методы верификации программ». В нем рассмотрены различные вопросы и методы формальной верификации программ, в частности, методы дедуктивной верификации, язык спецификации ACSL и инструменты Frama-C и Jessie. Пособие можно скачать на сайте кафедры СП.

Экзамен

15 июня состоится экзамен. Он пройдет в письменной форме. Экзамен начнется в 9:00 и будет проходить в течение 120 минут в аудитории 713. На экзамене вы можете использовать письменные и печатные материалы, но не можете использовать электронную технику и средства связи.

Вариант экзамена состоит из двух частей. В первой части вам нужно будет доказывать полную корректность блок-схем при помощи методов Флойда. Во второй части вам нужно будет работать с требованиями и спецификациями на языке ACSL.

Если будет много желающих писать экзамен, показ работ придется перенести на 16 июня.

Если вы хотите просто проставить оценку за работу в семестре, подходите в течение экзамена. Можно передать зачетную книжку через других студентов.

Отмена занятия

18 мая занятия не состоятся. Для согласования времени встреч для сдачи практического задания пишите мне на почту

Контрольная работа по ACSL

4 мая в 14:35 состоится контрольная работа по ACSL. Можно пользоваться любыми печатными и письменными материалами, нельзя пользоваться компьютерами и телефонами. Длительность работы — 40 минут. После этого можно будет сдавать первый этап практического задания.

Завершена проверка

Экспресс, предложенный на лекции 16 марта, и контрольная работа №1 проверены. Домашняя работа, собиравшаяся на лекции 16 марта, будет проверена позже.