Задача 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, из этой теории.