Метка: домашние-работы-2019

В архиве по этой ссылке находятся исходные файлы для выполнения задания:

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

Читать далее «Домашняя работа №8»

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

Задача 1. Дана блок-схема над 1 входной переменной, 1 промежуточной переменной и 1 выходной переменной. Домены всех переменных — множество всех целых чисел. Сигнатура \(mc91\) имеет домены аргументов и результатов — множества всех целых чисел. При помощи методов Флойда докажите полную корректность этой блок-схемы относительно спецификации \(\varphi(x) \equiv T\), \(\psi(x, z) \equiv (x \geq 101 \Rightarrow z = x — 10) \land (x < 101 \Rightarrow  z = 91)\), если сигнатуре \(mc91\) сопоставлена данная блок-схема.

Решение (теорию со всем необходимым, а также сессию доказательства) присылайте на почту до 23:59 22 марта. Требования к оформлению решения те же, что и в прошлой домашней работе.

Задача 1. Дана блок-схема над 2 входными переменными, 2 промежуточными переменными и 1 выходной переменной (алгоритм Евклида). Домены всех переменных — целочисленные. При помощи методов Флойда докажите полную корректность этой блок-схемы относительно спецификации \(\varphi(x_1,~x_2) \equiv x_1 > 0 \land x_2 > 0\), \(\psi(x_1, x_2, z_1) \equiv (z_1 = gcd(x_1, x_2))\). Функциональному символу \(gcd\) сопоставлена функция, вычисляющая наибольший общий делитель двух чисел. Это определяется в этой теории Why3.

Решение (теорию с индуктивными утверждениями, оценочными функциями, условиями (в виде целей) и комментариями, а также сессию доказательства) присылайте на почту до 23:59 15 марта. Требования к оформлению решения те же, что и в прошлой домашней работе. В вашей теории нужно импортировать теорию gcd по ссылке выше. Солверы сами смогут использовать аксиомы, определяющие символ gcd, из этой теории.

Задача 1. Дана блок-схема над 2 входными переменными, 2 промежуточными переменными и 1 выходной переменной. Домены всех переменных — целочисленные. При помощи метода индуктивных утверждений докажите частичную корректность этой блок-схемы относительно спецификации \(\varphi(x_1,~x_2) \equiv T\), \(\psi(x_1,~x_2,~z_1) \equiv (z_1 = x_1 * x_2)\).

Решение присылайте на почту до 23:59 10 марта. В вашем письме должен быть архив, в котором расположен файл с целями на языке Why3 и директория с сессией, в которой все цели доказаны. Ниже дано пояснение, что это такое, и требования к оформлению решения.

Читать далее «Домашняя работа №4»

Задача 1. Написать блок-схему, которая является обще полностью корректной относительно спецификации \((\varphi,~\psi)\) при заданной \(\gamma\), и доказать это. Блок-схема имеет три входные переменные \(x_1, x_2, x_3\) и одну выходную переменную \(z_1\). Домен переменных \(x_1\) и \(z_1\) обозначим как \(M\), домен переменных \(x_2\) и \(x_3\) обозначим как \(A\). Элементы множества \(M\) можно сравнивать на равенство, то же справедливо для множества \(A\). Других операций для этих множеств не определено.

Обратите внимание на то, что в спецификациях используются функциональные и предикатные символы и наборы аксиом. Это означает, что эти символы нельзя использовать для определения вычисления и, поэтому, нельзя использовать в качестве функций, приписанных операторам блок-схемы.

Функциональные и предикатные символы:
\(select: M \times A \rightarrow V\)
\(store: M \times A \times V \rightarrow M\)
\(valid: M \times A \rightarrow \{T, F\}\)

Элементы множества \(V\) можно сравнивать на равенство, других операций для этого множества не определено.

Аксиомы над указанными символами:
\(Ax1: \forall m \in M, a \in A, v \in V \cdot valid(m, a) \Rightarrow select(store(m, a, v), a) = v\)
\(Ax2: \forall m \in M, a, b \in A, v \in V \cdot valid(m, a) \land valid(m, b) \land a \neq b \\ \Rightarrow select(store(m, a, v), b) = select(m, b)\)
\(Ax3: \forall m \in M, a, b \in A, v \in V \cdot valid(m, a) \land valid(m, b) \\ \Rightarrow valid(store(m, a, v), b)\)

\(\varphi(x_1, x_2, x_3) \equiv valid(x_1, x_2) \land valid(x_1, x_3)\)
\(\psi(x_1, x_2, x_3, z_1) \equiv valid(z_1, x_2) \land valid(z_1, x_3) \\
\land select(z_1, x_2) = select(x_1, x_3) \land select(z_1, x_3) = select(x_1, x_2) \\ \land \forall x \in A \cdot x \neq x_2 \land x \neq x_3 \land valid(z_1, x) \land valid(x_1, x) \Rightarrow select(z_1, x) = select(x_1, x)\)

Сигнатуры для операторов CALL и их спецификации:

• \((DEREF, M \times A, V)\)
  • \(\varphi_{DEREF}(m, a) \equiv valid(m, a)\)
  • \(\psi_{DEREF}(m, a, v) \equiv v = select(m, a)\)
• \((SETREF, M \times A \times V, M)\)
  • \(\varphi_{SETREF}(m, a, v) \equiv valid(m, a)\)
  • \(\psi_{SETREF}(m, a, v, m’) \equiv m’ = store(m, a, v)\)

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

Задача 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.3.2(j), №1.3.3(e). Решения присылайте на до 23:59 15 февраля.