Задача 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 и директория с сессией, в которой все цели доказаны. Ниже дано пояснение, что это такое, и требования к оформлению решения.
Платформа Why3 состоит из языка Why3 для формулирования утверждений и инструментов для их доказательства. Собственно доказательством занимаются инструменты-солверы, не входящие в платформу Why3. Солверы отличаются тем, какие виды утверждений они готовы доказывать. Поэтому необходима среда для управления солерами: какое утверждение дать для доказательства какому солверу, как преобразовать (разделить) утверждение, чтобы оно лучше подходило для того или иного солвера. Цель проекта Why3 — сделать такую среду. Разные солверы имеют разные входные языки, но при доказательстве даже одного утверждения могут потребоваться разные солверы. Поэтому необходим единый язык для формулирования доказываемых утверждений (это и есть язык Why3) и транслятор под входной язык каждого солвера. Такие трансляторы входят в платформу Why3.
Инструкция по установке платформы Why3 и солверов расположена на сайте ИСП РАН. По этой ссылке находится описание языка Why3 (раздел 6) и среды Why3 IDE (раздел 1)
По этой ссылке можно скачать файл на языке Why3 для примера с лекции.
Ваше решение должно быть оформлено следующим образом:
- каждое условие верификации должно быть оформлено отдельным goal;
- из имени goal должно быть понятно, какому базовому пути соответствует его условие верификации;
- каждое индуктивное утверждение должно быть оформлено как predicate;
- перед каждым индуктивным утверждением должен быть комментарий с указанием связки блок-схемы, которой оно сопоставлено.
Ваши цели должны доказываться как минимум одним из следующих солверов: Alt-Ergo, Z3, CVC3, CVC4. Среда Why3 запоминает состояние процесса доказательства целей в виде сессии. Имея сессию, можно повторить доказательство.