Докажите, что эта блок-схема (картинка) полностью корректна относительно этой спецификации при помощи методов Флойда. Решение присылайте на почту до 12:00 17 марта в виде двух файлов: файла *.py с индуктивными утверждениями и оценочными функциями в формате PyFloyd и 2 файла *.prf с PVS доказательством истинности условий из метода индуктивных утверждений и метода фундированных множеств. Индуктивные утверждения в файле *.py должны годиться и для доказательства частичной корректности, и для доказательства завершаемости.
Обратите внимание, что команда PVS (grind) не применяет аксиомы и леммы. При необходимости можно добавить аксиому или лемму в список антецедентов при помощи команды (lemma) и продолжить доказательство при помощи (grind).
Для поддержки частичных функций обновите инструмент PyFloyd.