Статья 371

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

Понятие правильной программы первое знакомство.

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