Skip to main content
SpringerLink
Log in

Specifications and their use in defining subtypes

  • Object-Orientation
  • Conference paper
  • First Online:
ZUM '95: The Z Formal Specification Notation (ZUM 1995)

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

Included in the following conference series:

  • 174 Accesses

Abstract

Specifications are useful because they allow reasoning about objects without concern for their implementations. Type hierarchies are useful because they allow types that share common properties to be designed as a family. This paper is concerned with the interaction between specifications and type hierarchies. We present a way of specifying types, and show how some extra information, in addition to specifications of the objects' methods, is needed to support reasoning. We also provide a new way of showing that one type is a subtype of another. Our technique makes use of information in the types' specifications and works even in a very general computational environment in which possibly concurrent users share mutable objects.

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. Pierre America. Designing an object-oriented programming language with behavioural subtyping. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, REX School/Workshop, Noordwijkerhout, The Netherlands, May/June 1990, volume 489 of LNCS, pages 60–90. Springer-Verlag, NY, 1991.

    Google Scholar 

  2. Andrew P. Black, Norman Hutchinson, Eric Jul, Henry M. Levy, and Larry Carter. Distribution and abstract types in Emerald. IEEE TSE, 13(1):65–76, January 1987.

    Google Scholar 

  3. K.B. Bruce and P. Wegner. An algebraic model of subtype and inheritance. In Francois Bancilhon and Peter Buneman, editors, Advances in Database Programming Language, pages 75–96. Addison-Wesley, Reading, MA, 1990.

    Google Scholar 

  4. Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988.

    Google Scholar 

  5. D. Carrington, D. Duke, R. Duke, P. King, G. Rose, and P. Smith. Object-Z: An object oriented extension to Z. In FORTE89, International Conference on Formal Description Techniques, December 1989.

    Google Scholar 

  6. Elspeth Cusack. Inheritance in object oriented Z. In Proceedings of ECOOP '91. Springer-Verlag, 1991.

    Google Scholar 

  7. Elspeth Cusack and Michael Lai. Object-oriented specification in LOTOS and Z, or my cat really is object-oriented! In J. W. de Bakker, W. P de Roever, and G. Rozenberg, editors, Foundations of Object Oriented Languages, pages 179–202. Springer Verlag, June 1991. LNCS 489.

    Google Scholar 

  8. Krishna Kishore Dhara. Subtyping among mutable types in object-oriented programming languages. Master's thesis, Iowa State University, Ames, Iowa, 1992. Master's Thesis.

    Google Scholar 

  9. Krishna Kishore Dhara and Gary T. Leavens. Subtyping for mutable types in object-oriented programming languages. Technical Report 92-36, Department of Computer Science, Iowa State University, Ames, Iowa, November 1992.

    Google Scholar 

  10. David Duke and Roger Duke. A history model for classes in object-Z. In Proceedings of VDM '90: VDM and Z. Springer-Verlag, 1990.

    Google Scholar 

  11. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Springer-Verlag, 1985.

    Google Scholar 

  12. J.A. Goguen, C. Kirchner, H. Kirchner, A. Megrelis, J. Meseguer, and T. Winkler. An introduction to OBJ3. In J.-P. Jouannaud and S. Kaplan, editors, Proceedings, Conference on Conditional Term Rewriting, pages 258–263. Springer-Verlag, 1988. LNCS 308.

    Google Scholar 

  13. Joseph A. Goguen and Jose Meseguer. Unifying functional, object-oriented and relational programming with logical semantics. In Bruce Shriver and Peter Wegner, editors, Research Directions in Object Oriented Programming. MIT Press, 1987.

    Google Scholar 

  14. John V. Guttag, James J. Horning, and Jeannette M. Wing. The Larch family of specification languages. IEEE Software, 2(5):24–36, September 1985.

    Google Scholar 

  15. Gary Leavens. Verifying object-oriented prograsm that use subtypes. Technical Report 439, MIT Laboratory for Computer Science, February 1989. Ph.D. thesis.

    Google Scholar 

  16. Gary T. Leavens. Modular specification and verification of object-oriented programs. IEEE Software, 8(4):72–80, July 1991.

    Google Scholar 

  17. Gary T. Leavens and Krishna Kishore Dhara. A foundation for the model theory of abstract data types with mutation and aliasing (preliminary version). Technical Report 92-35, Department of Computer Science, Iowa State University, Ames, Iowa, November 1992.

    Google Scholar 

  18. Gary T. Leavens and William E. Weihl. Reasoning about object-oriented programs that use subtypes. In ECOOP/OOPSLA '90 Proceedings, 1990.

    Google Scholar 

  19. B. Liskov. Preliminary design of the Thor object-oriented database system. In Proc. of the Software Technology Conference. DARPA, April 1992. Also Programming Methodology Group Memo 74, MIT Laboratory for Computer Science, Cambridge, MA, March 1992.

    Google Scholar 

  20. B. Liskov, R. Atkinson, T. Bloom, E. Moss, J.C. Schaffert, R. Scheifler, and A. Snyder. CLU Reference Manual. Springer-Verlag, 1981.

    Google Scholar 

  21. B. Liskov and J. Guttag. Abstraction and Specification in Program Design. MIT Press, 1985.

    Google Scholar 

  22. Barbara Liskov and Jeannette M. Wing. A new definition of the subtype relation. In Proceedings of ECOOP '93, pages 118–141, Kaiserslautern, Germany, July 1993. Springer-Verlag. LNCS 707.

    Google Scholar 

  23. David Maier and Jacob Stein. Development and implementation of an object-oriented DBMS. In S.B. Zdonik and D. Maier, editors, Readings in Object-Oriented Database Systems, pages 167–185. Morgan Kaufmann, 1990.

    Google Scholar 

  24. Craig Schaffert, Topher Cooper, Bruce Bullis, Mike Kilian, and Carrie Wilpolt. An introduction to Trellis/Owl. In Proceedings of OOPSLA '86, pages 9–16, September 1986.

    Google Scholar 

  25. John Scheid and Steven Holtsberg. Ina Jo specification language reference manual. Technical Report TM-6021/001/06, Paramax Systems Corporation, A Unisys Company, June 1992.

    Google Scholar 

  26. J.M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 1989.

    Google Scholar 

  27. Mark Utting. An Object-Oriented Refinement Calculus with Modular Reasoning. PhD thesis, University of New South Wales, Australia, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory for Computer Science, Massachusetts Institute of Technology, 545 Technology Square, 02139, Cambridge, MA, USA

    Barbara Liskov

  2. Computer Science Department, Carnegie Mellon University, 5000 Forbes Avenue, 15213, Pittsburgh, PA, USA

    Jeannette M. Wing

Authors
  1. Barbara Liskov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jeannette M. Wing
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jonathan P. Bowen Michael G. Hinchey

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Liskov, B., Wing, J.M. (1995). Specifications and their use in defining subtypes. In: Bowen, J.P., Hinchey, M.G. (eds) ZUM '95: The Z Formal Specification Notation. ZUM 1995. Lecture Notes in Computer Science, vol 967. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60271-2_124

Download citation

  • DOI: https://doi.org/10.1007/3-540-60271-2_124

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60271-2

  • Online ISBN: 978-3-540-44782-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation