Specification techniques for data abstractions
- 1 April 1975
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 10 (6) , 72-87
- https://doi.org/10.1145/390016.808426
Abstract
The main purposes in writing this paper are to discuss the importance of formal specifications and to survey a number of promising specification techniques. The role of formal specifications both in proofs of program correctness, and in programming methodologies leading to programs which are correct by construction, is explained. Some criteria are established for evaluating the practical potential of specification techniques. The importance of providing specifications at the right level of abstraction is discussed, and a particularly interesting class of specification techniques, those used to construct specifications of data abstractions, is identified. A number of specification techniques for describing data abstractions are surveyed and evaluated with respect to the criteria. Finally, directions for future research are indicated.This publication has 15 references indexed in Scilit:
- Inductive methods for proving properties of programsCommunications of the ACM, 1973
- Relational level data structures for programming languagesActa Informatica, 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
- The design of the Venus operating systemCommunications of the ACM, 1972
- Toward an understanding of data structuresCommunications of the ACM, 1971
- The programming language pascalActa Informatica, 1971
- Proof of a programCommunications of the ACM, 1971
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- The structure of the “THE”-multiprogramming systemCommunications of the ACM, 1968