Lightweight Analysis of Object Interactions

  • Daniel Jackson
  • Alan Fekete
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)


The state of the practice in object-oriented software development has moved beyond reuse of code to reuse of conceptual structures such as design patterns. This paper draws attention to some difficulties that need to be solved if this style of development is to be supported by formal methods. In particular, the centrality of object interactions in many designs makes traditional reasoning less useful, since classes cannot be treated fruitfully in isolation from one another. We propose some ideas towards dealing with these issues: a relational model of heap structure capable of expressing sharing and mutual influence between objects; a declarative specification style that works in the presence of collaboration; and a tool-supported constraint analysis to expose problems in a diagram that captures, at a design level, a pattern of interaction. We illustrate these ideas with an example taken from a program used in the formatting of this paper.


Model Checker Design Pattern Method Call Frame Condition Object Interaction 
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.


  1. [1]
    M. Fayad and D. Schmid, Object-Oriented Application Frameworks, Special Issue, Communications of the ACM, 40(10), October 1997.Google Scholar
  2. [2]
    E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns, Addison Wesley, 1995Google Scholar
  3. [3]
    R. Helm, I. M. Holland, and D. Gangopadhyay. Contracts: Specifying Behavioral Compositions in Object Oriented Systems. European Conference on Object-Oriented Programming / ACM SIGPLANConfer ence on Object-Oriented Programming Systems, Languages, and Applications, Ottawa, Canada, Vol. 1, June 1990, 169–180.CrossRefGoogle Scholar
  4. [4]
    C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271–81, 1972.zbMATHCrossRefGoogle Scholar
  5. [5]
    Daniel Jackson. Object Models as Heap Invariants. In: Carroll Morgan and Annabelle McIver (eds.), Essays on Programming Methodology, Springer Verlag, 2000.Google Scholar
  6. [6]
    Daniel Jackson. Automating first-order relational logic. ACM SIGSOFT Conference on Foundations of Software Engineering, San Diego, California, November 2000.Google Scholar
  7. [7]
    Daniel Jackson. Alloy: A Lightweight Object Modelling Notation. To appear, ACM Transactions on Software Engineering and Methodology, October 2001.Google Scholar
  8. [8]
    Daniel Jackson, Ilya Shlyakhter and Manu Sridharan. A Micromodularity Mechanism. ACM SIGSOFT Conference on Foundations of Software Engineering / European Software Engineering Conference, Vienna, Austria, September 2001.Google Scholar
  9. [9]
    Daniel Jackson, Ian Schechter and Ilya Shlyakhter. Alcoa: the Alloy Constraint Analyzer. International Conference on Software Engineering, Limerick, Ireland, June 2000.Google Scholar
  10. [10]
    Daniel Jackson & Mandana Vaziri. Finding Bugs with a Constraint Solver. International Symposium on Software Testing and Analysis, Portland, Oregon, August 2000.Google Scholar
  11. [11]
    Daniel Jackson and Jeannette Wing. Lightweight Formal Methods. In: H. Saiedian (ed.), An Invitation to Formal Methods, IEEE Computer, 29(4):16–30, April 1996.Google Scholar
  12. [12]
    Gary T. Leavens. An overview of Larch/C++: Behavioral specifications for C++ modules. In: H. Kilovand W. Harvey (eds.), Specification of Behavioral Semantics in ObjectOriented Information Modeling, Amsterdam, Holland, 1996, Kluwer, pp.121–142.Google Scholar
  13. [13]
    Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design. In: Haim Kilov, Bernhard Rumpe, and Ian Simmonds (eds.), Behavioral Specifications of Businesses and Systems, Kluwer, 1999, Chapter 12, pp. 175–188.Google Scholar
  14. [14]
    K. Rustan M. Leino. Toward Reliable Modular Programs. Ph.D. thesis, California Institute of Technology, January 1995.Google Scholar
  15. [15]
    K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC/Java User’s Manual. Technical Note 2000-002, Compaq Systems Research Center, October 2000.Google Scholar
  16. [16]
    Barbara Liskovwith John Guttag. Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, 2001.Google Scholar
  17. [17]
    Bertrand Meyer. Object-Oriented Software Construction (2nd ed.). Prentice Hall, 1997.Google Scholar
  18. [18]
    Robert O’Callahan. Generalized Aliasing as a Basis for Program Analysis Tools. PhD thesis. Technical Report CMU-CS-01-124, School of Computer Science, Carnegie mellon University, Pittsburgh, PA, May 2001.Google Scholar
  19. [19]
    G. Ramalingam, Alex Warshavsky, John Field and Mooly Sagiv. Toward Effective Component Verification: Deriving an Efficient Program Analysis from a High-level Specification. Unpublished manuscript.Google Scholar
  20. [20]
    James Rumbaugh, Ivar Jacobson and Grady Booch. The Unified Modeling Language Reference Manual. Addison-Wesley, 1999.Google Scholar
  21. [21]
    M. Sagiv, T. Reps, and R. Wilhelm. Parametric Shape Analysis via 3-Valued Logic. ACM Symposium on Principles of Programming Languages, San Antonio, Texas, Jan. 20-22, 1999, ACM, New York, NY, 1999.Google Scholar
  22. [22]
    Allison Waingold. Lightweight Extraction of Object Models from Bytecode. Masters thesis, Department of Electrical Engineering and Computer Science, MIT, May 2001.Google Scholar
  23. [23]
    John Whaley and Martin Rinard. Compositional Pointer and Escape Analysis for Java Programs. ACM SIGPLANConfer ence on Object-Oriented Programming Systems, Languages, and Applications, Denver, Colorado, November 1999.Google Scholar
  24. [24]
    The Bandera Project. Kansas State University.
  25. [25]
    The SLAM Project. Microsoft Research.

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Daniel Jackson
    • 1
  • Alan Fekete
    • 2
  1. 1.Laboratory for Computer ScienceMassachusetts Institute of TechnologyCambridgeUSA
  2. 2.Basser Dept. of Computer ScienceUniversity of SydneySydneyAustralia

Personalised recommendations