Proof of a Program: FIND

A proof is given of the correctness of the
algorithm "Find."  First, a 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.

CACM January, 1971

Hoare, C. A. R.

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

4.0 4.22 5.21 5.23 5.24

CA710107 JB February 8, 1978  10:40 AM

2021	4	2227
2222	4	2227
2227	4	2227
2227	4	2227
2315	4	2227
2326	4	2227
2470	4	2227
2732	4	2227
2783	4	2227
2865	4	2227
2896	4	2227
2943	4	2227
3014	4	2227
3054	4	2227
3068	4	2227
3077	4	2227
3143	4	2227
1834	5	2227
307	5	2227
2227	5	2227
2227	5	2227
2227	5	2227
2356	5	2227
2420	5	2227
2874	5	2227
3143	5	2227
970	6	2227
1491	6	2227
1682	6	2227
1834	6	2227
2227	6	2227
2227	6	2227
2227	6	2227
2227	6	2227
2317	6	2227
2683	6	2227
2871	6	2227
521	6	2227