Skip to main content
SpringerLink
Log in

Object models as heap invariants

  • Chapter
Programming Methodology

Part of the book series: Monographs in Computer Science ((MCS))

Abstract

Object models are widely used for describing structural properties of object-oriented programs, but they suffer from two problems. First, their semantics is usually unclear. Second, the textual constraints that are often used to annotate diagrams are not integrated with the diagrammatic notation itself. In this paper, we show how to interpret an object model as a heap invariant by translation to a small relational logic. With a few additional shorthands, this logic can be used for textual constraints, so that annotation is just conjunction. Our semantics is simpler than those proposed by others, and accounts for features of the object model that have not been addressed in treatments that focus on more abstract models.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 149.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Serge Abiteboul and Richard Hull. IFO: A Formal Semantic Database Model. ACM Transactions on Database Systems,Vol. 12, No. 4, December 1987, pp. 525–565.

    Article  Google Scholar 

  2. Robert H. Bourdeau and Betty H.C. Cheng. A Formal Semantics for Object Model Diagrams. IEEE Transactions on Software Engineering, October 1995.

    Google Scholar 

  3. Derek Coleman, Patrick Arnold, Stephanie Bodoff, Chris Dollin, Helena Gilchrist, Fiona Hayes and Paul Jeremaes. Object-Oriented Development: The Fusion Method. Prentice Hall, 1994.

    Google Scholar 

  4. Steve Cook and John Daniels. Designing Object Systems: Object-Oriented Modelling with Syntropy. Prentice Hall, 1994.

    MATH  Google Scholar 

  5. Peter P. Chen. The Entity-Relationship Model-Toward a Unified View of Data. ACM Transactions on Database Systems, Vol. 1, No. 1, (1976), pp. 9–36.

    Article  MathSciNet  Google Scholar 

  6. David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended Static Checking. Research Report 159, Compaq Systems Research Center, December, 1998.

    Google Scholar 

  7. Desmond F. D’Souza and Alan Cameron Wills. Objects, Components and Frameworks With UML: The Catalysis Approach. Addison-Wesley, 1998.

    Google Scholar 

  8. Robert B. France, Jean-Michel Bruel, Maria M. Larrondo-Petrie, and Malcolm Shroff. Exploring the Semantics of UML Type Structures with Z. Proceedings of the Formal Methods for Open Object-based Distributed Systems (FMOODS’97), Canterbury, England, July 1997. Chapman & Hall, 1997.

    Google Scholar 

  9. Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison Wesley, October 1994.

    Google Scholar 

  10. John V. Guttag, James J. Horning, and Andres Modet. Report on the Larch Shared Language: Version 2.3. Technical Report 58, Compaq Systems Research Center, Palo Alto, CA, 1990.

    Google Scholar 

  11. Ali Hamie, John Howse and Stuart Kent. Interpreting the Object Constraint Language. Proceedings of Asia Pacific Conference in Software Engineering, IEEE Press, 1998.

    Google Scholar 

  12. Ali Hamie, John Howse and Stuart Kent. Navigation expressions in object-oriented modelling. Proceedings Fundamental Approaches to Software Engineering (FASE’98), European Joint Conferences on the Theory and Practice of Software(ETAPS’98), Lisbon, Portugal, March 1998. LNCS 1382, Springer-Verlag, 1998.

    Google Scholar 

  13. Michael Hammer and Dennis McLeod. Database description with SDM: a semantic database model. ACM Transactions on Database Systems, Vol. 6, No. 2, June 1981, pp. 351–386.

    Article  Google Scholar 

  14. C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1 (4), pp. 271–281, 1972.

    Article  MATH  Google Scholar 

  15. C.A.R. Hoare and Jifeng He. A trace model for pointers and objects. Proc. 13th European Conference on Object-Oriented Programming, Lisbon, Portugal, June 14–18, 1999. LNCS 1628, Springer-Verlag, 1999. Reprinted in this volume.

    Google Scholar 

  16. Daniel Jackson. Alloy: A Lightweight Object Modelling Notation. Technical Report 797, MIT Laboratory for Computer Science, Cambridge, MA, February 2000. Latest version available at: http://sdg.lcs.mit.edu/~dnj/publications. To appear, ACM Transactions on Software Engineering.

    Google Scholar 

  17. Daniel Jackson. Automating first-order relational logic. Proc. ACM SIGSOFT Conf. Foundations of Software Engineering. San Diego, November 2000.

    Google Scholar 

  18. Stuart Kent, Stephen Gaito, Niall Ross. A meta-model semantics for structural constraints in UML. In H. Kilov, B. Rumpe, and I Sinmionds, editors, Behavioral specifications for businesses and systems, chapter 9, pages 123–141. Kluwer Academic Publishers, Norwell, MA, September 1999.

    Google Scholar 

  19. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: a behavioral interface specification language for Java. Department of Computer Science, Iowa State University, TR #98–06j, June 1998, revised May 2000. Available at http://www.cs.iastate.eduh/~leavens.

    Google Scholar 

  20. Barbara Liskov with John Guttag. Program Development in Java. Addison-Wesley, 2001.

    Google Scholar 

  21. E.-R. Olderog and A.P. Ravn. Documenting design refinement. Proc. ACM SIGSOFT Workshop on Formal Methods in Software Practice, Portland, Oregon, August 2000, pp. 89–100.

    Google Scholar 

  22. Mark Richters and Martin Gogolla. On Formalizing the UML Object Constraint Language OCL, Proc. 17th Int. Conf. Conceptual Modeling (ER’98), 1998, LNCS 1507, pp. 449–464, Springer-Verlag.

    Google Scholar 

  23. Martin Rinard and Viktor Kuncak. Object Models, Heaps and Interpretations. Technical Report 816, MIT Laboratory for Computer Science, Cambridge, Massachusetts, January 2001.

    Google Scholar 

  24. James Rumbaugh, Michael Blaha, William Premerlani, Frederick Eddy and William Lorensen. Object-Oriented Modeling and Design. Prentice Hall, 1991.

    Google Scholar 

  25. James Rumbaugh, Ivar Jacobson and Grady Booch. The Unified Modeling Language Reference Manual. Addison-Wesley, 1999.

    Google Scholar 

  26. David W. Shipman. The Functional Data Model and the Data Language DAPLEX. ACM Transactions on Database Systems, Vol. 6, No. 1, March 1981, pp. 140–173.

    Article  Google Scholar 

  27. Malcolm Shroff and Robert B. France. Towards a formalization of UML class structures in Z. Proceedings of Twenty-First Annual International Computer Software and Applications Conference (COMPSAC’97), pages 646–651. IEEE Computer Society Press, 1997.

    Google Scholar 

  28. J. Michael Spivey. The Z Notation: A Reference Manual. Second edition, Prentice Hall, 1992.

    Google Scholar 

  29. Toby J. Teorey, DongQing Yang and James R. Fry. A logical design methodology for relational databases using the extended entity-relationship model. ACM Computing Surveys, 18(2), June 1986, pp. 197–222.

    Article  MATH  Google Scholar 

  30. Jos Warmer and Anneke Kleppe. The Object Constraint Language: Precise Modeling with UML. Addison Wesley, 1999.

    Google Scholar 

Download references

Authors
  1. Daniel Jackson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Macquarie University, 2109, Sydney, Australia

    Annabelle McIver

  2. Department of Computer Science and Engineering, The University of New South Wales, 2052, Sydney, Australia

    Carroll Morgan

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer Science+Business Media New York

About this chapter

Cite this chapter

Jackson, D. (2003). Object models as heap invariants. In: McIver, A., Morgan, C. (eds) Programming Methodology. Monographs in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-0-387-21798-7_12

Download citation

  • DOI: https://doi.org/10.1007/978-0-387-21798-7_12

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4419-2964-8

  • Online ISBN: 978-0-387-21798-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation