Срок сдачи этой домашней работы — семинар 17 марта.
Доказать полную корректность блок-схемы относительно заданного контракта. Доменом всех переменных является множество целых чисел.
Операция a % b означает остаток от деления a на b. Операция определена только для положительных b и неотрицательных a. Обозначение |a| означает модуль a.
φ(x) ≡ (x ≥ 0) ∧ (x % 2 = 1)
ψ(x, z) ≡ z = x2
