Proof of a Program: FIND
The work
| Authors | C. A. R. Hoare |
|---|---|
| Type | article |
| Year | 1971 |
| Citekey | hoare1971proof |
Where it appeared
| Published in | Communications of the ACM |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 14 |
| Issue | 1 |
| Pages | 39--45 |
Identifiers
| DOI | 10.1145/362452.362489 |
|---|
Related
| Distinct from | foley1971proof |
|---|
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.
A copy is held
pdf, 527.4 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | import via bibtex |
|---|---|
| Added | 2026-08-09 00:00 UTC |
| Approved by | a person 2026-08-28 21:27 UTC |
Filed under
Cite it as
@article{hoare1971proof,
title = {Proof of a Program: FIND},
author = {C. A. R. Hoare},
year = {1971},
journal = {Communications of the ACM},
volume = {14},
number = {1},
pages = {39--45},
publisher = {Association for Computing Machinery},
doi = {10.1145/362452.362489},
}
This record lives at https://refs.drheap.org/hoare1971proof/ and will keep doing so.