An example of hierarchical design and proof
- 1 December 1978
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 21 (12) , 1064-1075
- https://doi.org/10.1145/359657.359667
Abstract
Hierarchical programming is being increasingly recognized as helpful in the construction of large programs. Users of hierarchical techniques claim or predict substantial increases in productivity and in the reliability of the programs produced. In this paper we describe a formal method for hierarchical program specification, implementation, and proof. We apply this method to a significant list processing problem and also discuss a number of extensions to current programming languages that ease hierarchical program design and proof.Keywords
This publication has 16 references indexed in Scilit:
- Abstract data types and the development of data structuresCommunications of the ACM, 1977
- Proof techniques for hierarchically structured programsCommunications of the ACM, 1977
- Modula: A language for modular multiprogrammingSoftware: Practice and Experience, 1977
- Proving Properties of Complex Data StructuresJournal of the ACM, 1976
- The treatment of data types in EL1Communications of the ACM, 1974
- Inductive methods for proving properties of programsCommunications of the ACM, 1973
- Protection in programming languagesCommunications of the ACM, 1973
- On the criteria to be used in decomposing systems into modulesCommunications of the ACM, 1972
- A technique for software module specification with examplesCommunications of the ACM, 1972
- Integrity of a Mass Storage Filing SystemThe Computer Journal, 1969