Четвёртая домашняя работа блока методов Флойда

Срок сдачи этой домашней работы — семинар 17 марта.

Доказать полную корректность блок-схемы относительно заданного контракта. Доменом всех переменных является множество целых чисел.

Операция a % b означает остаток от деления a на b. Операция определена только для положительных b и неотрицательных a. Обозначение |a| означает модуль a.

φ(x) ≡ (x ≥ 0) ∧ (x % 2 = 1)
ψ(x, z) ≡ z = x2

hw-floyd-4

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *