Class-local object invariants

ABSTRACT

The correctness of object-oriented programs relies on object invariants. A system for verifying such programs requires a systematic method for coping with object invariants that can be violated temporarily. This paper describes a sound methodology for flexibly changing data locally in object structures, supporting programming patterns that occur frequently in practice. In more detail, to handle subclasses, previous approaches have been geared toward programs that update the fields of an object only in overridable virtual methods of the object. The enhanced methodology in this paper handles field updates in a much more flexible way. The flexibility can be applied to a field in the common case where the field is not mentioned in subclass invariants

REFERENCES

• 1: Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and KRustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, volume 4111 of Lecture Notes in Computer Science, pages 364--387. Springer, September 2006.
• 2: Mike Barnett, Robert DeLine, Manuel Fähndrich, KRustan M. Leino, and Wolfram Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27--56, 2004.
• 3: Mike Barnett, KRustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean, editors, CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices, volume 3362 of Lecture Notes in Computer Science, pages 49--69. Springer, 2005.
• 4: Mike Barnett and David A. Naumann. Friends need a bit more: Maintaining invariants over shared state. In Dexter Kozen and Carron Shankland, editors, Mathematics of Program Construction, 7th International Conference, MPC 2004, volume 3125 of Lecture Notes in Computer Science, pages 54--84. Springer, July 2004.
• 5: Andrew D. Birrell. An introduction to programming with threads. Research Report 35, Digital Equipment Corporation Systems Research Center, January 1989.
• 6: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 7: David Gerard Clarke, Object ownership and containment, University of New South Wales, New South Wales, Australia, 2003
• 8: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.48-64, October 18-22, 1998, Vancouver, British Columbia, Canada
• 9: Ádám Darvas and KRustan M. Leino. Practical reasoning about invocations and implementations of pure methods. In Matthew B. Dwyer and Antónia Lopes, editors, Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, volume 4422 of Lecture Notes in Computer Science, pages 336--351. Springer, March 2007.
• 10: Bart Jacobs , Frank Piessens , K. Rustan M. Leino , Wolfram Schulte, Safe Concurrency for Aggregate Objects with Invariants, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.137-147, September 07-09, 2005 [doi>10.1109/SEFM.2005.39]
• 11: Bart Jacobs and Frank Piessens. Verification of programs with inspector methods. In Workshop on Formal Techniques for Java-like Programs (FTfJP 2006), July 2006.
• 12: Bart Jacobs, Jan Smans, Frank Piessens, and Wolfram Schulte. A statically verifiable programming model for concurrent object-oriented programs. In Zhiming Liu and Jifeng He, editors, Formal Methods and Software Engineering, 8th International Conference on Formal Engineering Methods, ICFEM 2006, volume 4260 of Lecture Notes in Computer Science, pages 420--439. Springer, November 2006.
• 13: Ioannis T. Kassios. Dynamic frames: Support for framing, dependencies and sharing without restrictions. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM 2006: Formal Methods, 14th International Symposium on Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 268--283. Springer, August 2006.
• 14: K. Rustan M. Leino and Peter Müller. Object invariants in dynamic contexts. In Martin Odersky, editor, ECOOP 2004 -- Object-Oriented Programming, 18th European Conference, volume 3086 of Lecture Notes in Computer Science, pages 491--516. Springer, June 2004.
• 15: K. Rustan M. Leino and Peter Müller. Modular verification of static class invariants. In John Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors, FM 2005: Formal Methods, International Symposium of Formal Methods Europe, volume 3582 of Lecture Notes in Computer Science, pages 26--42. Springer, July 2005.
• 16: K. Rustan M. Leino and Wolfram Schulte. Using history invariants to verify observers. In Rocco De~Nicola, editor, Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, volume 4421 of Lecture Notes in Computer Science, pages 80--94. Springer, March 2007.
• 17: Ronald Middelkoop, Cornelis Huizing, Ruurd Kuiper, and Erik Luit. Invariants for non-hierarchical object structures. In Anamaria Martins Moreira and Leila Ribeiro, editors, Brazilian Symposium on Formal Methods, SBMF 2006, pages 233--248. SBC, September 2006.
• 18: Peter Müller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of Lecture Notes in Computer Science. Springer-Verlag, 2002.
• 19: Peter Müller and Arnd Poetzsch-Heffter. Universes: A type system for alias and dependency control. Technical Report 279, FernUniversität Hagen, 2001.
• 20: Peter Müller , Arnd Poetzsch-Heffter , Gary T. Leavens, Modular invariants for layered object structures, Science of Computer Programming, v.62 n.3, p.253-286, 15 October 2006 [doi>10.1016/j.scico.2006.03.001]
• 21: Matthew Parkinson , Gavin Bierman, Separation logic and abstraction, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.247-258, January 12-14, 2005, Long Beach, California, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Class invariants

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers; Programming by contract

General Terms:
Languages, Verification

Keywords:
automation, object-oriented programming, specification, subclassing, tool support, verification