Статья 397

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