Home → Magazine Archive → January 1971 (Vol. 14, No. 1) → Proof of a program: FIND → Abstract

Proof of a program: FIND

By C. A. R. Hoare

Communications of the ACM, Vol. 14 No. 1, Pages 39-45

Save PDF
A proof is given of the correctness of the algorithm “Find.” First, an informal description is given of the purpose of the program and the method used. A systematic technique is described for constructing the program proof during the process of coding it, in such a way as to prevent the intrusion of logical errors. The proof of termination is treated as a separate exercise. Finally, some conclusions relating to general programming methodology are drawn.

The full text of this article is premium content


No entries found