384 Reliability of programs.
2 juli 1973. 3 pages.
Reliability must be considered a mathematical statement in all aspects: to be general and precise, and to have a tradition of proof with theorems, axioms, and proven patterns of reasoning.
We can use results of computer processing only if we are certain that the underlying programs are correct. Initially one believed in proof by testing, but because testing all cases is impossible, testing as a method for ensuring correctness is unacceptable. Methods for correctness proofs took off after the discovery that program structure was the key: Don’t try to prove a completed program, but create the program and its correctness proof simutaneously.
One of the most powerful tools is the invariance theorem for loops by C.A.R. Hoare: If for the statement S the condition P and B is a sufficient pre-condition to ensure that the post-condition P is satisfied, then for the statement while B do S od the pre-condition P is sufficient to ensure the post-condition P, if S terminates.
The theorem is very important, because the proof doesn’t have to express how effective the step towards non B is. This “strategic abstraction” is being used more and more.
An example of a program to find the convex hull of a nonempty set of points on a plane concludes the article.
—MB