Домашняя работа №2

Задача 1. Для блок-схемы с семинара определить множество всех \(\gamma\) («гамма»), при которых эта блок-схема будет обще частично корректна относительно спецификации \(\varphi(x)~\equiv~T,~\psi(x, z)~\equiv~F\). Определить множество всех \(\gamma\), при которых эта блок-схема будет обще полностью корректна относительно той же спецификации.

Задача 2. Пусть есть некоторые целочисленные константы \(MIN\) и \(MAX\) такие, что \(MIN<0<MAX~\land~MIN+MAX~=~-1\). Написать блок-схему над 3 входными переменными \(x_1,~x_2,~x_3\) и 1 выходной переменной \(z_1\) (промежуточные переменные выбрать самостоятельно). Домены всех переменных — множество всех целых чисел. Блок-схема должна быть обще полностью корректна относительно спецификации \((\varphi,~\psi)\) при указанной ниже \(\gamma\). В блок-схеме можно использовать лишь следующие функции: константные (в том числе, \(MIN\) и \(MAX\)), равные одному из своих аргументов, арифметические сравнения двух целых чисел. В блок-схеме можно использовать указанные ниже сигнатуры.

Спецификация: \(\varphi(x_1,~x_2,~x_3)~\equiv~MIN\leq x_1 \leq MAX~\land~MIN\leq x_2 \leq MAX~\land\)
\(MIN\leq x_3 \leq MAX~\land~MIN\leq x_1 + x_2 — x_3 \leq MAX\),
\(\psi(x_1,~x_2,~x_3,~z_1)~\equiv~(z_1~=~x_1 + x_2 — x_3)\).

Сигнатуры:
(ADD, \(D_{arg}~=~\mathbb{Z}~\times~\mathbb{Z}\), \(D_{res}~=~\mathbb{Z}\))
(SUB, \(D_{arg}~=~\mathbb{Z}~\times~\mathbb{Z}\), \(D_{res}~=~\mathbb{Z}\))

\(\gamma(ADD)~=~(\varphi_{ADD},~\psi_{ADD})\)
\(\varphi_{ADD}(a,~b)~\equiv~MIN\leq a \leq MAX~\land~MIN\leq b \leq MAX~\land~MIN\leq a + b \leq MAX\)
\(\psi_{ADD}(a,~b,~c)~\equiv~(c~=~a + b)\)
\(\varphi_{SUB}(a,~b)~\equiv~MIN\leq a \leq MAX~\land~MIN\leq b \leq MAX~\land~MIN\leq a — b \leq MAX\)
\(\psi_{SUB}(a,~b,~c)~\equiv~(c~=~a — b)\)

Решения присылайте на до 23:59 22 февраля.

Домашняя работа №1

Решите следующие задачи из задачника: №1.3.2(j), №1.3.3(e). Решения присылайте на до 23:59 15 февраля.

Экзамен

14 июня состоится экзамен. Он пройдет в аудитории 706 и начнется в 9:00. Экзамен длится 120 минут. За это время можно доказать полную корректность блок-схемы при помощи методов Флойда (10 баллов) и написать спецификацию типа данных и Си-функций при помощи языка ACSL (15 баллов). Можно пользоваться любыми письменными и напечатанными материалами. Нельзя пользоваться электронной техникой.

Проверена контрольная работа

Результаты контрольной работы №2 можно посмотреть в таблице с баллами. Сканы работ с комментариями можно посмотреть по этой ссылке: https://www.dropbox.com/sh/3f547cchfdievy1/AAB76SzmhqhHoomMyNQ-OdBWa?dl=0

Контрольная работа по языку Си

19 апреля состоится контрольная работа №2. За полтора часа надо будет решить несколько задач.

Одна задача посвящена спецификации интерфейса модуля на языке Си: спецификации глобальных переменных, типов и функций при помощи языка ACSL. Необходимо понимать, что интерфейсу соответствует не одна реализация, а множество реализаций.

Другая — доказать, что некоторая заданная реализация функции с циклом соответствует заданной спецификации. Нужно будет дополнить реализацию аннотациями на языке ACSL. Для решения этой задачи нужно уметь применять методы Флойда в ACSL.

Работа выполняется без использования компьютера. Можно использовать свои конспекты, иные материалы на бумаге. Электронными материалами и спедствами связи пользоваться нельзя.

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

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

Практическое задание

Всем разосланы письма с их вариантами заданий. Первый этап — это спецификация типов и функций. Второй этап — доказательство того, что реализация типа и функций соответствует спецификации. Реализацию можно получить после приема преподавателем первого этапа. Сдавать первый этап можно уже 19 апреля после контрольной работы. Занятия после 19 апреля будут посвящены только приему практического задания. Если в какой-то из дней никто не придет в течение 15 минут после начала занятия, преподаватель покидает аудиторию.

Продление срока

Так как лекция 5 апреля была посвящена вопросам спецификации и верификации программ с указателями, срок сдачи домашнего задания №3 по языку Си сдвигается на 12:00 16 апреля.