Proof of a program: FIND

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.

REFERENCES

• 1: NAUR, P. Proof of algorithms by general snapshots. BIT 6 (1966) 310-316.
• 2: DIJKSTRA, E. W. A constructive approach to the problem of program correctness. BIT 8 (1968), 174-186.
• 3: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 4: C. A. R. Hoare, Algorithm 65: find, Communications of the ACM, v.4 n.7, p.321-322, July 1961 [doi>10.1145/366622.366647]
• 5: NAUR, P. Programming by action clusters. BIT 9 (1969), 25O-258.
• 6: DIJKSTRA, E. W. Structured Programming {EWD249} T.H.E. (privately circulated).
• 7: FLOYD, R. W. Assigning meanings to programs. Proc. Amer. Math. Soc. Symposium in Applied Mathematics, Vol. 19, pp. 19-31.
• 8: James Cornelius King, A program verifier, 1970

INDEX TERMS

Keywords:
program correctness, program documentation, programming methodology, proofs of programs, theory of programming