Separation logic, abstraction and inheritance

ABSTRACT

Inheritance is a fundamental concept in object-oriented programming, allowing new classes to be defined in terms of old classes. When used with care, inheritance is an essential tool for object-oriented programmers. Thus, for those interested in developing formal verification techniques, the treatment of inheritance is of paramount importance. Unfortunately, inheritance comes in a number of guises, all requiring subtle techniques.

To address these subtleties, most existing verification methodologies typically adopt one of two restrictions to handle inheritance: either (1) they prevent a derived class from restricting the behaviour of its base class (typically by syntactic means) to trivialize the proof obligations; or (2) they allow a derived class to restrict the behaviour of its base class, but require that every inherited method must be reverified. Unfortunately, this means that typical inheritance-rich code either cannot be verified or results in an unreasonable number of proof obligations.

In this paper, we develop a separation logic for a core object-oriented language. It allows derived classes which override the behaviour of their base class, yet supports the inheritance of methods without reverification where this is safe. For each method, we require two specifications: a static specification that is used to verify the implementation and direct method calls (in Java this would be with a super call); and a dynamic specification that is used for calls that are dynamically dispatched; along with a simple relationship between the two specifications. Only the dynamic specification is involved with behavioural subtyping. This simple separation of concerns leads to a powerful system that supports all forms of inheritance with low proof-obligation overheads. We both formalize our methodology and demonstrate its power with a series of inheritance examples.

REFERENCES

• 1: M. Barnett, R. DeLine, M. Fähndrich, K. R. M. Leino, and W. Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27--56, 2004.
• 2: M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In Proceedings of CASSIS, pages 49--69, 2005.
• 3: Bodil Biering , Lars Birkedal , Noah Torp-Smith, BI-hyperdoctrines, higher-order separation logic, and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.5, p.24-es, August 2007 [doi>10.1145/1275497.1275499]
• 4: G. M. Bierman, M. J. Parkinson, and A. M. Pitts. MJ: An imperative core calculus for Java and Java with effects. Technical Report 563, University of Cambridge Computer Laboratory, 2004.
• 5: Wei-Ngan Chin , Cristina David , Huu Hai Nguyen , Shengchao Qin, Enhancing modular OO verification with separation logic, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 6: William R. Cook , Walter Hill , Peter S. Canning, Inheritance is not subtyping, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.125-135, December 1989, San Francisco, California, United States [doi>10.1145/96709.96721]
• 7: Krishna Kishore Dhara , Gary T. Leavens, Forcing behavioral subtyping through specification inheritance, Proceedings of the 18th international conference on Software engineering, p.258-267, March 25-29, 1996, Berlin, Germany
• 8: Cormac Flanagan , Amr Sabry , Bruce F. Duba , Matthias Felleisen, The essence of compiling with continuations, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.237-247, June 21-25, 1993, Albuquerque, New Mexico, United States
• 9: M. Flatt, S. Krishnamurthi, and M. Felleisen. A programmer's reduction semantics for classes and mixins. Technical Report TR-97-293, Rice University, 1997. Corrected June, 1999.
• 10: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 11: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 12: Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-26, January 2001, London, United Kingdom
• 13: N. Krishnaswami, J. Aldrich, and L. Birkedal. Modular verification of the subject-observer pattern via higher-order separation logic. In Proceedings of FTfJP, 2007.
• 14: G.T. Leavens and D.A. Naumann. Behavioral subtyping is equivalent to modular reasoning for object-oriented programs. Technical Report TR-06-36, Iowa State University, 2006.
• 15: Gary T. Leavens , Albert L. Baker , Clyde Ruby, Preliminary design of JML: a behavioral interface specification language for java, ACM SIGSOFT Software Engineering Notes, v.31 n.3, May 2006 [doi>10.1145/1127878.1127884]
• 16: K. Rustan M. Leino, Data groups: specifying the modification of extended state, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.144-153, October 18-22, 1998, Vancouver, British Columbia, Canada
• 17: K. R. M. Leino and P. Müller. A verification methodology for model fields. In Proceedings of ESOP, 2006.
• 18: K. R. M. Leino and W. Schulte. Using history invariants to verify observers. In Proceedings of ESOP, 2007.
• 19: Barbara H. Liskov , Jeannette M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.6, p.1811-1841, Nov. 1994 [doi>10.1145/197320.197383]
• 20: Peter Müller, Modular specification and verification of object-oriented programs, Springer-Verlag New York, Inc., New York, NY, 2002
• 21: 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]
• 22: A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract predicates and mutable ADTs in Hoare Type Theory. In Proceedings of ESOP, 2007.
• 23: Peter W. O'Hearn , John C. Reynolds , Hongseok Yang, Local Reasoning about Programs that Alter Data Structures, Proceedings of the 15th International Workshop on Computer Science Logic, p.1-19, September 10-13, 2001
• 24: M. Parkinson, G. Bierman, J. Noble, and W. Schulte. Contracts for patterns. Unpublished note, 2007.
• 25: M. J. Parkinson. Local Reasoning for Java. PhD thesis, Computer Laboratory, University of Cambridge, 2005. UCAM-CL-TR-654.
• 26: 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
• 27: Arnd Poetzsch-Heffter , Peter Müller, A Programming Logic for Sequential Java, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.162-176, March 22-28, 1999
• 28: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 29: Clyde Ruby , Gary T. Leavens, Safely creating correct subclasses without seeing superclass code, ACM SIGPLAN Notices, v.35 n.10, p.208-228, Oct. 2000
• 30: Hongseok Yang , Uday S. Reddy, Local reasoning for stateful programs, University of Illinois at Urbana-Champaign, Champaign, IL, 2001

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Inheritance; Classes and objects

General Terms:
Languages, Theory, Verification

Keywords:
classes, modularity, separation logic