Lightweight Analysis of Object Interactions
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.
KeywordsModel Checker Design Pattern Method Call Frame Condition Object Interaction
Unable to display preview. Download preview PDF.
- M. Fayad and D. Schmid, Object-Oriented Application Frameworks, Special Issue, Communications of the ACM, 40(10), October 1997.Google Scholar
- E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns, Addison Wesley, 1995Google Scholar
- 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
- Daniel Jackson. Object Models as Heap Invariants. In: Carroll Morgan and Annabelle McIver (eds.), Essays on Programming Methodology, Springer Verlag, 2000.Google Scholar
- Daniel Jackson. Automating first-order relational logic. ACM SIGSOFT Conference on Foundations of Software Engineering, San Diego, California, November 2000.Google Scholar
- Daniel Jackson. Alloy: A Lightweight Object Modelling Notation. To appear, ACM Transactions on Software Engineering and Methodology, October 2001.Google Scholar
- 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
- Daniel Jackson, Ian Schechter and Ilya Shlyakhter. Alcoa: the Alloy Constraint Analyzer. International Conference on Software Engineering, Limerick, Ireland, June 2000.Google Scholar
- Daniel Jackson & Mandana Vaziri. Finding Bugs with a Constraint Solver. International Symposium on Software Testing and Analysis, Portland, Oregon, August 2000.Google Scholar
- 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
- 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
- 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
- K. Rustan M. Leino. Toward Reliable Modular Programs. Ph.D. thesis, California Institute of Technology, January 1995.Google Scholar
- 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
- Barbara Liskovwith John Guttag. Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, 2001.Google Scholar
- Bertrand Meyer. Object-Oriented Software Construction (2nd ed.). Prentice Hall, 1997.Google Scholar
- 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
- 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
- James Rumbaugh, Ivar Jacobson and Grady Booch. The Unified Modeling Language Reference Manual. Addison-Wesley, 1999.Google Scholar
- 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
- Allison Waingold. Lightweight Extraction of Object Models from Bytecode. Masters thesis, Department of Electrical Engineering and Computer Science, MIT, May 2001.Google Scholar
- 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
- The Bandera Project. Kansas State University. http://www.cis.ksu.edu/santos/bandera/.
- The SLAM Project. Microsoft Research. http://www.research.microsoft.com/projects/slam/.