Статья 412

Требуется доказать тотальную правильность программы при данных пред- и постусловиях, доказать утверждение. Докажем вначале, что при истинном предусловии возникновение в программе бесконечных циклов исключается. Бесконечные циклы могли возникнуть либо в области действия оператора, либо из-за использования операторов безусловного перехода то в том случае, если они заставляют вновь и вновь, без конца возвращаться к уже выполнявшимся ранее строкам программы. Но выполнение любого из имеющихся в программе операторов, то ведет к окончанию работы будет выполнен оператор. Остается проверить единственный содержащийся в цикл.
Окончание цикла строки зависит от выполнения условия. Из предусловия следует, что целое число. Если реализуется случай, выполнение строки программы завершится переходом к строке, минуя цикл.