Proof techniques for hierarchically structured programs
- 1 April 1977
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 20 (4), 271-283
- https://doi.org/10.1145/359461.359483
Abstract
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.This publication has 20 references indexed in Scilit:
- An example of hierarchical design and proofCommunications of the ACM, 1978
- Use of the concept of transparency in the design of hierarchically structured systemsCommunications of the ACM, 1975
- Reasoning about programsArtificial Intelligence, 1974
- MonitorsCommunications of the ACM, 1974
- The treatment of data types in EL1Communications of the ACM, 1974
- A technique for software module specification with examplesCommunications of the ACM, 1972
- Program development by stepwise refinementCommunications of the ACM, 1971
- Procedures and parameters: An axiomatic approachLecture Notes in Mathematics, 1971
- Certification of algorithm 245 [M1]:treesort 3:proof of algorithms—a new kind of certificationCommunications of the ACM, 1970
- Algorithm 245: TreesortCommunications of the ACM, 1964