CACM logo

This Article

Communications of the ACM

Proof of a program: FIND

C. A. R. Hoare

January 1, 1971

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.
Read the Full Article:
Abstract  |  Full Text (PDF)  |  In the Digital Library

Tools For Readers

Bookmark and Share
Default Font Size Large Font Size X-Large Font Size Text Size
Author profiles and more in the Digital Library

About Communications | Join ACM External Link | Renew External Link | Subscribe External Link | Sign In | For Authors | For Advertisers External Link | Privacy | Site Map | Help | Contact Us | Mobile Site

Copyright © 2012 by the ACM. All rights reserved.

Back to Top