Статья 400

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

называется

называется

Говорить о правильности программы самой по себе бессмысленно если не иметь в виду отсутствие синтаксических ошибок, авоста или бесконечных циклов.