Notes on Type Abstraction (Version 2)
- 1 January 1980
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. SE-6 (1) , 13-23
- https://doi.org/10.1109/tse.1980.230209
Abstract
This paper, which was initially prepared to accompany a series of lectures given at the 1978 NATO International Summer School on Program Construction, is primarily tutorial in nature. It begins by discussing in a general setting the role of type abstraction and the need for formal specifications of type abstractions. It then proceeds to examine in some detail two approaches to the construction of such specifications: that proposed by Hoare in his 1972 paper "Proofs of Correctness of Data Representations," and the author's own version of algebraic specifications. The Hoare approach is presented via a discussion of its embodiment in the programming language Euclid. The discussion of the algebraic approach includes material abstracted from earlier papers as well as some new material that has yet to appear. This new material deals with parameterized types and the specification of restrictions. The paper concludes with a brief discussion of the relative merits of the two approaches to type abstraction.Keywords
This publication has 12 references indexed in Scilit:
- Data Type Specification: Parameterization and the Power of Specification TechniquesACM Transactions on Programming Languages and Systems, 1982
- Abstract data types and software validationCommunications of the ACM, 1978
- The algebraic specification of abstract data typesActa Informatica, 1978
- Proof rules for the programming language EuclidActa Informatica, 1978
- Abstract data types and the development of data structuresCommunications of the ACM, 1977
- Types are not setsPublished by Association for Computing Machinery (ACM) ,1973
- A technique for software module specification with examplesCommunications of the ACM, 1972
- Proof of correctness of data representationsActa Informatica, 1972
- Simple Word Problems in Universal Algebras††The work reported in this paper was supported in part by the U.S. Office of Naval Research.Published by Elsevier ,1970
- An axiomatic basis for computer programmingCommunications of the ACM, 1969