Skip to main content
SpringerLink
Log in

Object-oriented implementation of abstract data type specifications

  • Conference
  • Conference paper
  • First Online:
Algebraic Methodology and Software Technology (AMAST 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1101))

  • 159 Accesses

Abstract

We present a method for implementing abstract data type specifications by object-oriented programs and for proving implementation correctness. The method uses an algebraic description of the semantics of object-oriented programs which allows one to relate an abstract data type specification and its object-oriented implementation within a common formal framework. On this algebraic level the correctness of an implementation can be proved using the notion of observational implementation and its associated proof techniques.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Bidoit, R. Hennicker: Modular correctness proofs of behavioural implementations. Available by WWW: http://www.pst.informatik.uni-muenchen.de/∼hennicke/, 1995. A short version appeared as: Proving the correctness of behavioural implementations. Proc. AMAST '95, Springer Lecture Notes in Computer Science 936, 152–168, 1995.

    Google Scholar 

  2. M. Bidoit, R. Hennicker: Behavioural theories and the proof of behavioural properties. To appear in Theor. Comp. Science. Previous version in: Report LIENS-95-5, Ecole Normale Supérieure, 1995.

    Google Scholar 

  3. M. Bidoit, R. Hennicker, M. Wirsing: Behavioural and abstractor specifications. Science of Computer Programming 25 (2–3), 149–186, 1995.

    Google Scholar 

  4. R. Breu: Algebraic Specification Techniques in Object Oriented Programming Environments. Springer Lecture Notes in Computer Science 562, 1991.

    Google Scholar 

  5. R. Breu, E. Zucca: An Algebraic Compositional Semantics of an Object Oriented Notation with Concurrency. In: C. E. Veni Madhavan (ed.): Proc. 9th Conf. on Foundations of Software Technology and Theoretical Computer Science, Springer Lecture Notes in Computer Science 405, 131–142, 1990.

    Google Scholar 

  6. H. Ehrig, B. Mahr: Fundamentals of algebraic specification 1, EATCS Monographs on Theoretical Computer Science 6, Springer, 1985.

    Google Scholar 

  7. J. Guttag, J. Horning: Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science, Springer, 1993.

    Google Scholar 

  8. J. A. Goguen, J. Meseguer: Universal realization, persistent interconnection and implementation of abstract modules. In Proc. ICALP '82, Springer Lecture Notes in Computer Science 140, 265–281, 1982.

    Google Scholar 

  9. J. A. Goguen, J. Meseguer: Unifying functional, object-oriented and relational programming with logical semantics. In: B. Shriver, P. Wegner (eds.): Research Directions in Object-Oriented Programming, 417–477, MIT Press, 1987.

    Google Scholar 

  10. R. Hennicker: Context induction: a proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing 3 (4), 326–345, 1991.

    Google Scholar 

  11. R. Hennicker, C. Schmitz: Object-oriented implementation of abstract data type specifications. Extended version of this paper. Available by WWW: http://www.pst.informatik.unimuenchen.de/∼hennicke/, 1996.

    Google Scholar 

  12. R. Jungclaus, G. Saake, T. Hartmann and C. Sernadas: Object-oriented specification of information systems: The TROLL language. Informatik-Bericht 91-04, Technische Universität Braunschweig, 1991.

    Google Scholar 

  13. G. Kreisel, J. L. Krivine: Eléments de Logique Mathematique. Dunod (Paris), 1967.

    Google Scholar 

  14. U. Lechner, C. Lengauer and M. Wirsing: An object-oriented airport: specification and refinement in Maude. In: E. Astesiano, G. Reggio, A. Tarlecki (eds.): Recent Trends in Data Type Specification, Springer Lecture Notes in Computer Science 906, 351–367, 1995.

    Google Scholar 

  15. J. Meseguer: A logical theory of concurrent objects and its realization in the Maude language. In: G. Agha, P. Wegner and A. Yonezawa (eds.): Research Directions in Object-Based Concurrency, MIT Press, 314–390, 1993.

    Google Scholar 

  16. B. Meyer: Programming for reusability and extendibility. Sigplan Notices 22 (2), 85–94, 1987.

    Google Scholar 

  17. B. Meyer: Eiffel: the language. Prentice Hall International, 1992.

    Google Scholar 

  18. G. Malcolm, J. A. Goguen: Proving correctness of refinement and implementation. Technical Monograph PRG-114, Oxford University Computing Laboratory, 1994.

    Google Scholar 

  19. P. Nivela, F. Orejas: Initial behaviour semantics for algebraic specifications. In: D. T. Sannella, A. Tarlecki (eds.): Proc. 5th Workshop on Algebraic Specifications of Abstract Data Types, Springer Lecture Notes in Computer Science 332, 184–207, 1988.

    Google Scholar 

  20. H. Reichel: Initial computability, algebraic specifications, and partial algebras. International Series of Monographs in Computer Science No. 2, Oxford: Clarendon Press, 1987.

    Google Scholar 

  21. D. T. Sannella, A. Tarlecki: Toward formal development of programs from algebraic specifications: implementation revisited. Acta Informatica 25, 233–281, 1988.

    Google Scholar 

  22. M. Wirsing: Structured algebraic specifications: a kernel language. Theoretical Computer Science 42, 123–249, 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Ludwig-Maximilians-Universität München, Oettingenstr. 67, D-80538, München, Germany

    Rolf Hennicker

  2. Wilhelm-Schickard-Institut, Universität Tübingen, Sand 13, D-72076, Tübingen, Germany

    Christoph Schmitz

Authors
  1. Rolf Hennicker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Schmitz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Martin Wirsing Maurice Nivat

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hennicker, R., Schmitz, C. (1996). Object-oriented implementation of abstract data type specifications. In: Wirsing, M., Nivat, M. (eds) Algebraic Methodology and Software Technology. AMAST 1996. Lecture Notes in Computer Science, vol 1101. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014314

Download citation

  • DOI: https://doi.org/10.1007/BFb0014314

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61463-0

  • Online ISBN: 978-3-540-68595-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation