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. P. America. Designing an object-oriented programming language with behavioural subtyping. In the REX School/Worshop on Foundations of Object-Oriented Languages, pages 60--90, 1991.
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. K.K. Dhara and G.T. Leavens. Forcing behavioral subtyping through specification inheritance. In IEEE/ACM Intl. Conf. on Software Engineering, pages 258--267, 1996.
6. J.C. Filliâtre. Why: a multi-language multi-prover verification tool. Technical Report 1366, LRI, Université Paris Sud, March 2003.
7. R.B. Findler and M. Felleisen. Contract soundness for object--oriented languages. In SIGPLAN Object--Oriented Programming Systems, Languages and Applications, pages 1--15, 2001.
8. R.B. Findler, M. Latendresse, and M. Felleisen. Behavioral contracts and behavioral subtyping. In ESEC/SIGSOFT Foundations of Software Engr., 2001.
9. C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata. Extended Static Checking for Java. In ACM PLDI, June 2002.
10. J. Hatcliff, X. Deng, M.B. Dwyer, G. Jung, and V.P. Ranganath. Cadena: An integrated development, analysis, and verification environment for component-based systems. In IEEE/ACM Intl. Conf. on Software Engineering, 2003.
11. S. Isthiaq and P.W. O'Hearn. BI as an assertion language for mutable data structures. In ACM POPL, London, January 2001.
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. G.T. Leavens and Peter Muller. Information hiding and visibility in interface specifications. In IEEE/ACM Intl. Conf. on Software Engineering, pages 385--395, Washington, DC, USA, 2007. IEEE Computer Society.
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. G.T. Leavens, A.L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes, 31 (3):1--38, 2006.
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. B.H. Liskov. Data abstraction and hierarchy. ACM SIGPLAN Notices, 23(5):17--34, May 1988. Revised version of the keynote address given at OOPSLA'87.
19. B.H. Liskov and J.M. Wing. A behavioral notion of subtyping. ACM Trans. on Programming Languages and Systems, 16 (6):1811--1841, 1994.
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. B. Meyer. Object-oriented Software Construction. Prentice Hall. Second Edition., 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. P. Muller. Modular specification and verification of object-oriented programs. Springer, New York, NY, USA, 2002. ISBN 3-540-43167-5.
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. J.W. Nimmer and M.D. Ernst. Invariant inference for static checking. In ESEC/SIGSOFT Foundations of Software Engr., pages 11--20, 2002.
27. P.W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1--3):271--307, 2007.
28. P.W. O'Hearn, H. Yang, and J.C. Reynolds. Separation and Information Hiding. In ACM POPL, Venice, Italy, January 2004.
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. M.J. Parkinson and G.M. Bierman. Separation logic and abstraction. In ACM POPL, pages 247--258, 2005.
32. M.J. Parkinson and G.M. Bierman. Separation logic, abstraction and inheritance. In ACM POPL, 2008.
33. C. Pasareanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In SPIN Workshop, April 2004.
34. W. Pugh. The Omega Test: A fast practical integer programming algorithm for dependence analysis. Communications of the ACM, 8:102--114, 1992.
35. J. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In IEEE Logic in Computer Science, Copenhagen, Denmark, July 2002.
36. Robby, M. B. Dwyer, and J. Hatcliff. Bogor: an extensible and highly-modular software model checking framework. In ESEC/SIGSOFT Foundations of Software Engr., pages 267--276, 2003.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • General programming languages

      • Language features

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program verification