Abstract
In this paper, we present a new semantics for the implementation of abstract data types. This semantics leads to a simple, exhaustive description of the abstract implementation correctness criteria. These correctness criteria are expressed in terms of sufficient completeness and hierarchical consistency. Thus, correctness proofs of abstract implementations can always be handled using classical tools such as theorem proving methods, structural induction methods or syntactical methods (e.g. fair presentations). The main idea of our approach is the use of intermediate “concrete sorts”, which synthesize the available values used by implementation. Moreover, we show that the composition of several correct abstract implementations is always correct. This provides a formal foundation for a methodology of program development by stepwise refinement.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
12. References
Goguen J., Thatcher J., Wagner E.: “An initial algebra approach to the specification, correctness, and implementation of abstract data types”, Current Trends in Programming Methodology, Vol.4, Yeh Ed. Prentice Hall, 1978 (also IBM Report RC 6487, Oct. 1976).
Ehrig H., Kreowski H., Thatcher J., Wagner J., Wright J.: “Parameterized data types in algebraic specification languages”, Proc. 7th ICALP, July 1980.
Bernot G.: “Une sémantique algébrique pour une spécification différenciée des exceptions et des erreurs: application à l'implémentation et aux primitives de structuration des spécifications formelles”, Thèse de troisième cycle, Université de Paris-Sud, Orsay, 1985.
Bidoit M.: “Algebraic data types: structured specifications and fair presentations”, Proc. of AFCET Symposium on Mathematics for Computer Science, Paris, March 1982.
Ehrig H., Kreowski H., Mahr B., Padawitz P.: “Algebraic implementation of abstract data types”, Theoretical Computer Science, Oct. 1980.
Ehrig H., Kreowski H., Padawitz P.: “Algebraic implementation of abstract data types: concept, syntax, semantics and correctness”, Proc. ICALP, Springer-Verlag LNCS 85, 1980.
Gaudel M.C.: “Génération et preuve de compilateurs basée sur une sémantique formelle des languages de programmation”, Thèse d'état, Nancy, 1980.
Guttag J.V., Horowitz E., Musser D.R.: “Abstract data types and software validation”, C.A.C.M., Vol 21, n.12, 1978. (also USG ISI Report 76-48).
Guttag J.V.: “The specification and application to programming”, Ph.D. Thesis, University of Toronto, 1975.
Liskov B., Zilles S.: “Specification techniques for data abstractions”, IEEE Transactions on Software Engineering, Vol.SE-1 N 1, March 1975.
Sanella D., Wirsing M.: “Implementation of parameterized specifications”, Report CSR-103-82, Department of Computer Science, University of Edinburgh.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bernot, G., Bidott, M., Choppy, C. (1985). Abstract implementations and correctness proofs. In: Monien, B., Vidal-Naquet, G. (eds) STACS 86. STACS 1986. Lecture Notes in Computer Science, vol 210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16078-7_80
Download citation
DOI: https://doi.org/10.1007/3-540-16078-7_80
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16078-6
Online ISBN: 978-3-540-39758-8
eBook Packages: Springer Book Archive