Proof of a program
- 1 January 1971
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 14 (1), 39-45
- https://doi.org/10.1145/362452.362489
Abstract
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.This publication has 6 references indexed in Scilit:
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- Programming by action clustersBIT Numerical Mathematics, 1969
- A constructive approach to the problem of program correctnessBIT Numerical Mathematics, 1968
- Assigning meanings to programsProceedings of Symposia in Applied Mathematics, 1967
- Proof of algorithms by general snapshotsBIT Numerical Mathematics, 1966
- Algorithm 65: findCommunications of the ACM, 1961