Enhancing modular OO verification with separation logic

ABSTRACT

Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in superclasses, leading to imprecision during program reasoning. To address this, we advocate a fresh approach to OO verification that focuses on the distinction and relation between specifications that cater to calls with static dispatching from those for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid code re-verification, where possible. Using a predicate mechanism, we propose a flexible scheme for supporting class invariant and lossless casting. Our aim is to lay the foundation for a practical verification system that is precise, concise and modular for sequential OO programs. We exploit the separation logic formalism to achieve this.

REFERENCES

• 1: Pierre America, Designing an Object-Oriented Programming Language with Behavioural Subtyping, Proceedings of the REX School/Workshop on Foundations of Object-Oriented Languages, p.60-90, May 28-June 01, 1990
• 2: M. Barnet, R. DeLine, M. Fahndrich, K.R.M Leino, and W. Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27--56, 2004.
• 3: M. Barnett, K.R.M. Leino, and W. Schulte. The Spec# programming system: An overview. In Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, 2004.
• 4: D.R. Cok and J. Kiniry. ESC/Java2: Uniting ESC/Java and JML. In Int'l Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pages 108--128, 2004.
• 5: 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
• 6: J.C. Filliâtre. Why: a multi-language multi-prover verification tool. Technical Report 1366, LRI, Université Paris Sud, March 2003.
• 7: Robert Bruce Findler , Matthias Felleisen, Contract Soundness for object-oriented languages, ACM SIGPLAN Notices, v.36 n.11, p.1-15, 11/01/2001
• 8: Robert Bruce Findler , Mario Latendresse , Matthias Felleisen, Behavioral contracts and behavioral subtyping, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 9: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 10: John Hatcliff , Xinghua Deng , Matthew B. Dwyer , Georg Jung , Venkatesh Prasad Ranganath, Cadena: an integrated development, analysis, and verification environment for component-based systems, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 11: 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
• 12: J. Kiniry, E. Poll, and D. Cok. Design by contract and automatic verification for Java with JML and ESC/Java2. ETAPS tutorial, 2005.
• 13: Gary T. Leavens , Peter Muller, Information Hiding and Visibility in Interface Specifications, Proceedings of the 29th international conference on Software Engineering, p.385-395, May 20-26, 2007 [doi>10.1109/ICSE.2007.44]
• 14: G.T. Leavens and David A. Naumann. Behavioral subtyping is equivalent to modular reasoning for object-oriented programs. Technical Report 06-36, Department of Computer Science, 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: G.T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, P. Müller, and J. Kiniry. JML Reference Manual (DRAFT), February 2007.
• 17: K.R.M. Leino and P. Müller. Object invariants in dynamic contexts. In ECOOP, pages 491--516, 2004.
• 18: Barbara Liskov, Keynote address - data abstraction and hierarchy, ACM SIGPLAN Notices, v.23 n.5, p.17-34, May 1988
• 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: C. Marché and C. Paulin-Mohring. Reasoning about Java programs with aliasing and frame conditions. In 18th Int'l Conf. on Theorem Proving in Higher Order Logics. Springer, LNCS, August 2005.
• 21: C. Marché, C. Paulin-Mohring, and X. Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58 (1--2):89--106, 2004.
• 22: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 23: R. Middelkoop, C. Huizing, R. Kuiper, and E.J. Luit. Invariants for non-hierarchical object structures. In L. Ribeiro and A. Martins Moreira, editors, Proceedings of the 9th Brazilian Symposium on Formal Methods (SBMF'06), Natal, Brazil, 2006.
• 24: Peter Müller, Modular specification and verification of object-oriented programs, Springer-Verlag New York, Inc., New York, NY, 2002
• 25: H.H. Nguyen, C. David, S.C. Qin, and W.N. Chin. Automated Verification of Shape And Size Properties via Separation Logic. In Intl Conf. on Verification, Model Checking and Abstract Interpretation, Nice, France, January 2007.
• 26: Jeremy W. Nimmer , Michael D. Ernst, Invariant inference for static checking:, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587054]
• 27: Peter W. OHearn, Resources, concurrency, and local reasoning, Theoretical Computer Science, v.375 n.1-3, p.271-307, May, 2007 [doi>10.1016/j.tcs.2006.12.035]
• 28: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 29: J. Ostroff, C. Wang, E. Kerfoot, and F.A. Torshizi. Automated model--based verification of object-oriented code. Technical Report CS-2006-05, York University, Canada, May 2006.
• 30: M.J. Parkinson. Local Reasoning for Java. PhD thesis, Computer Laboratory, University of Cambridge, 2005. UCAM-CL-TR-654.
• 31: 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
• 32: Matthew J. Parkinson , Gavin M. Bierman, Separation logic, abstraction and inheritance, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 33: C. Pasareanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In SPIN Workshop, April 2004.
• 34: William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, v.35 n.8, p.102-114, Aug. 1992 [doi>10.1145/135226.135233]
• 35: 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
• 36: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Languages, Theory, Verification

Keywords:
automated verification, enhanced subsumption, lossless casting, separation logic, static and dynamic specifications