Design patterns in separation logic

ABSTRACT

Object-oriented programs are notable for making use of both higher-order abstractions and mutable, aliased state. Either feature alone is challenging for formal verification, and the combination yields very flexible program designs and correspondingly difficult verification problems. In this paper, we show how to formally specify and verify programs that use several common design patterns in concert.

REFERENCES

• 1: M. Barnett, K. Leino, and W. Schulte. The Spec# Programming System: An Overview. Proceedings CASSIS 2004, 2005.
• 2: M. Barnett and D. Naumann. Friends Need a Bit More: Maintaining Invariants Over Shared State. Mathematics of Program Construction (MPC), 2004.
• 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: 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
• 5: B. Jacobs, E. Meijer, F. Piessens, and W. Schulte. Iterators revisited: Proof rules and implementation. Proceedings FTfJP, 2005.
• 6: N. Kokholm. An extended library of collection classes for .NET. Master's thesis, IT University of Copenhagen, Copenhagen, Denmark, 2004.
• 7: Neelakantan R. Krishnaswami, Reasoning about iterators with separation logic, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon [doi>10.1145/1181195.1181213]
• 8: N. R. Krishnaswami. The semantics of higher-order separation logic for a higher-order language. Technical report, Carnegie Mellon University, 2008.
• 9: Susan Eisenbach, Formal underpinnings of Java, Addendum to the 1998 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum), January 1998, Vancouver, British Columbia, Canada [doi>10.1145/346852.346968]
• 10: K. R. M. Leino and W. Schulte. Using history invariants to verify observers. In European Symposium on Programming (ESOP), pages 80--94. Springer, 2007.
• 11: Barbara H. Liskov , Jeannette M. Wing, Behavioural subtyping using invariants and constraints, Formal methods for distributed processing: a survey of object-oriented approaches, Cambridge University Press, New York, NY, 2001
• 12: A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract Predicates and Mutable ADTs in Hoare Type Theory. In In Proceedings of European Symposium on Programming'07, volume 4421 of Lecture Notes in Computer Science, pages 189--204. Springer, 2007.
• 13: Aleksandar Nanevski , Greg Morrisett , Lars Birkedal, Polymorphism and separation in hoare type theory, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 14: A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Reasoning with the awkward squad. In In Proceedings of International Conference on Functional Programming'08, 2008.
• 15: M. Parkinson. Local Reasoning for Java. PhD in Computer Science, University of Cambridge, August 2005.
• 16: M. Parkinson. Class invariants: The end of the road. Proceedings IWACO, 2007.
• 17: Matthew Parkinson , Gavin Bierman, Separation logic and abstraction, ACM SIGPLAN Notices, v.40 n.1, p.247-258, January 2005
• 18: Dino Distefano , Matthew J. Parkinson J, jStar: towards practical verification for java, Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications, October 19-23, 2008, Nashville, TN, USA
• 19: R. L. Petersen, L. Birkedal, A. Nanevski, and G. Morrisett. A realizability model for impredicative Hoare Type Theory. In In Proceedings of European Symposium on Programming'08, 2008.
• 20: Frank Pfenning , Rowan Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, v.11 n.4, p.511-540, August 2001 [doi>10.1017/S0960129501003322]
• 21: B. C. Pierce and D. N. Turner. Statically typed friendly functions via partially abstract types. Technical Report ECS-LFCS-93-256, University of Edinburgh, LFCS, Apr. 1993. Get by anonymous ftp from ftp.dcs.ed.ac.uk in pub/bcp/friendly.ps.Z. Also available as INRIA-Rocquencourt Rapport de Recherche No. 1899.
• 22: C. Pierik, D. Clarke, and F. de Boer. Creational Invariants. Proceedings FTfJP, 2004.
• 23: John C. Reynolds, An Introduction to Specification Logic, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.442, June 06-08, 1983
• 24: 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
• 25: Steve M. Shaner , Gary T. Leavens , David A. Naumann, Modular verification of higher-order methods with mandatory calls specified by model programs, Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 26: K. Svendsen, A. Buisse, and L. Birkedal. Verifying design patterns in Hoare Type Theory. Technical Report ITU-TR-2008-112, IT University of Copenhagen, sep 2008.

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

General Terms:
Languages, Verification

Keywords:
design patterns, separation logic