Home → Magazine Archive → April 1977 (Vol. 20, No. 4) → Proof techniques for hierarchically structured programs → Abstract

Proof techniques for hierarchically structured programs

By Lawrence Robinson, Karl N. Levitt

Communications of the ACM, Vol. 20 No. 4, Pages 271-283

Save PDF
A method for describing and structuring programs that simplifies proofs of their correctness is presented. The method formally represents a program in terms of levels of abstraction, each level of which can be described by a self-contained nonprocedural specification. The proofs, like the programs, are structured by levels. Although only manual proofs are described in the paper, the method is also applicable to semi-automatic and automatic proofs. Preliminary results are encouraging, indicating that the method can be applied to large programs, such as operating systems.

The full text of this article is premium content


No entries found