Статья 402

Так как компьютер умеет проверять истинность утверждения, тем самым в силу эквивалентности, содержащейся в постусловии дается ответ на вопрос о делимости.
Скажем несколько слов о частичной и тотальной правильности. Из определений следует, что всякая тотально правильная программа является частично правильной при тех же пред- и постусловиях. Обратное, конечно, не верно мы уже имели возможность убедиться в этом. По-видимому, все согласятся с тем, что тотальная правильность лучше частичной, хотя осуществить доказательство тотальной правильности сложнее это понятно ведь любое доказательство тотальной правильности содержит в себе доказательство частичной правильности и, кроме того, доказательство отсутствия бесконечных циклов.
Иногда утверждения о частичной правильности программ могут выглядеть довольно странно. Рассмотрим, например, следующий фрагмент программы обозначим его буквой.