Abstract implementations and correctness proofs

  • Gilles Bernot
  • Michel Bidott
  • Christine Choppy
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 210)


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.


Equality Representation Correctness Proof Abstract Data Type Concrete Operation Algebraic Specification 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

12. References

  1. [ADJ 76]
    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).Google Scholar
  2. [ADJ 80]
    Ehrig H., Kreowski H., Thatcher J., Wagner J., Wright J.: “Parameterized data types in algebraic specification languages”, Proc. 7th ICALP, July 1980.Google Scholar
  3. [Ber 85]
    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.Google Scholar
  4. [Bid 82]
    Bidoit M.: “Algebraic data types: structured specifications and fair presentations”, Proc. of AFCET Symposium on Mathematics for Computer Science, Paris, March 1982.Google Scholar
  5. [EKMP 80]
    Ehrig H., Kreowski H., Mahr B., Padawitz P.: “Algebraic implementation of abstract data types”, Theoretical Computer Science, Oct. 1980.Google Scholar
  6. [EKP 80]
    Ehrig H., Kreowski H., Padawitz P.: “Algebraic implementation of abstract data types: concept, syntax, semantics and correctness”, Proc. ICALP, Springer-Verlag LNCS 85, 1980.Google Scholar
  7. [Gau 80]
    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.Google Scholar
  8. [GHM 76]
    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).Google Scholar
  9. [Gut 75]
    Guttag J.V.: “The specification and application to programming”, Ph.D. Thesis, University of Toronto, 1975.Google Scholar
  10. [LZ 75]
    Liskov B., Zilles S.: “Specification techniques for data abstractions”, IEEE Transactions on Software Engineering, Vol.SE-1 N 1, March 1975.Google Scholar
  11. [SW 82]
    Sanella D., Wirsing M.: “Implementation of parameterized specifications”, Report CSR-103-82, Department of Computer Science, University of Edinburgh.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1985

Authors and Affiliations

  • Gilles Bernot
    • 1
  • Michel Bidott
    • 1
  • Christine Choppy
    • 1
  1. 1.Laboratoire de Recherche en InformatiqueUniversité PARIS-SUDOrsay CedexFrance

Personalised recommendations