Стоит доделать задание, которое разбиралось на семинаре.
Основное задание:
доказать методом индуктивных утверждений Флойда частичную корректность следующей блок-схемы относительно заданной спецификации.
φ(x) ≡ (x ≥ 0)
ψ(x, z) ≡ z2 ≤ x < (z + 1)2
Формальные методы разработки программ
Магистратура факультета ВМК МГУ имени М.В. Ломонсоова
Стоит доделать задание, которое разбиралось на семинаре.
Основное задание:
доказать методом индуктивных утверждений Флойда частичную корректность следующей блок-схемы относительно заданной спецификации.
φ(x) ≡ (x ≥ 0)
ψ(x, z) ≡ z2 ≤ x < (z + 1)2