Modular verification of higher-order methods with mandatory calls specified by model programs

ABSTRACT

What we call a''higher-order method" (HOM) is a method that makes mandatory calls to other dynamically-dispatched methods. Examples include template methods as in the Template method design pattern and notify methods in the Observer pattern. HOMs are particularly difficult to reason about, because standard pre- and postcondition specifications cannot describe the mandatory calls. For reasoning about such methods, existing approaches use either higher order logic or traces, but both are complex and verbose.

We describe a simple, concise, and modular approach to specifying HOMs We show how to verify calls to HOMs and their code using first-order verification conditions, in asound and modular way.

Verification of client code that calls HOMs can take advantage of the client's knowledge about the mandatory calls to make strong conclusions. Our verification technique validates and explains traditional documentation practice for HOMs, which typically shows their code. However, specifications do not have to expose all of the code to clients, but only enough to determine how the HOM makes its mandatory calls.

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: Ralph-Johan J. Back , Abo Akademi , J. Von Wright , F. B. Schneider , D. Gries, Refinement Calculus: A Systematic Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1998
• 3: Anindya Banerjee , David A. Naumann, Ownership confinement ensures representation independence for object-oriented programs, Journal of the ACM (JACM), v.52 n.6, p.894-960, November 2005 [doi>10.1145/1101821.1101824]
• 4: M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean, editors, Construction and Analysis of Safe, Secure, and Interoperable Smart devices (CASSIS 2004), volume 3362 of Lecture Notes in Computer Science, pages 49--69. Springer-Verlag, 2005.
• 5: Mike Barnett , Wolfram Schulte, Runtime verification of .NET contracts, Journal of Systems and Software, v.65 n.3, p.199-208, 15 March 2003 [doi>10.1016/S0164-1212(02)00041-9]
• 6: Bernhard Beckert , Reiner Hähnle , Peter H. Schmitt, Verification of Object-Oriented Software. The KeY Approach: Foreword by K. Rustan M. Leino (Lecture Notes in Computer Science), Springer-Verlag New York, Inc., Secaucus, NJ, 2007
• 7: M. Büchi. Safe language mechanisms for modularization and concurrency. Technical Report TUCS Dissertations No. 28, Turku Center for Computer Science, May 2000.
• 8: M. Büchi and W. Weck. A plea for grey-box components. Technical Report 122, Turku Center for Computer Science, Presented at the Workshop on Foundations of Component-Based Systems, Zürich, September 1997, 1997. http://tinyurl.com/2833tr.
• 9: Martin Buchi , Wolfgang Weck, The Greybox Approach: When Blackbox Specifications Hide Too Much, Turku Centre for Computer Science, 1999
• 10: Ana Cavalcanti , David A. Naumann, A Weakest Precondition Semantics for Refinement of Object-Oriented Programs, IEEE Transactions on Software Engineering, v.26 n.8, p.713-728, August 2000 [doi>10.1109/32.879810]
• 11: Patrice Chalin , Frédéric Rioux, Non-null references by default in the Java modeling language, Proceedings of the 2005 conference on Specification and verification of component-based systems, September 05-06, 2005, Lisbon, Portugal
• 12: W. Damm and B. Josko. A sound and relatively complete Hoare-logic for a language with higher type procedures. Acta Informatica, 20(1):59--101, Oct. 1983.
• 13: Frank S. de Boer, A WP-calculus for OO, Proceedings of the Second International Conference on Foundations of Software Science and Computation Structure, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, p.135-149, March 22-28, 1999
• 14: 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
• 15: G. W. Ernst, J. K. Navlakha, and W. F. Ogden. Verification of programs with procedure-type parameters. Acta Informatica, 18(2):149--169, Nov. 1982.
• 16: Robert Bruce Findler , Matthias Felleisen, Contracts for higher-order functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.48-59, October 04-06, 2002, Pittsburgh, PA, USA
• 17: 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
• 18: 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
• 19: E. C. R. Hehner. Specified blocks. Verified Software: Theories, Tools, Experiments (VSTTE), Oct. 2005. http://tinyurl.com/2a7kf2.
• 20: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 21: C. A. R. Hoare. Procedures and parameters: An axiomatic approach. In E. Engeler, editor, Symposium on Semantics of Algorithmic Languages. Springer-Verlag, 1971.
• 22: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 23: G. T. Leavens. JML's rich, inherited specifications for behavioral subtypes. In Z. Liu and H. Jifeng, editors, Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM), volume 4260 of Lecture Notes in Computer Science, pages 2--34, New York, NY, Nov. 2006. Springer-Verlag.
• 24: 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]
• 25: Gary T. Leavens , K. Rustan M. Leino , Peter Müller, Specification and verification challenges for sequential object-oriented programs, Formal Aspects of Computing, v.19 n.2, p.159-189, June 2007 [doi>10.1007/s00165-007-0026-7]
• 26: 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]
• 27: G. T. Leavens and D. A. Naumann. Behavioral subtyping, specification inheritance, and modular reasoning. Technical Report 06--20b, Department of Computer Science, Iowa State University, Ames, Iowa, 50011, Sept. 2006.
• 28: G. T. Leavens, D. A. Naumann, and S. Rosenberg. Preliminary definition of Core JML. CS Report 2006--07, Stevens Institute of Technology, Sept. 2006.
• 29: G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. R. Cok, P. Müller, J. Kiniry, and P. Chalin. JML Reference Manual. Department of Computer Science, Iowa State University. Available from http://www.jmlspecs.org, Feb. 2007.
• 30: G. T. Leavens and W. E. Weihl. Specification and verification of Object-Oriented programs using supertype abstraction. Acta Informatica, 32(8):705--778, Nov. 1995.
• 31: 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
• 32: 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]
• 33: C. Morgan, Procedures, parameters, and abstraction: separate concerns, Science of Computer Programming, v.11 n.1, p.17-27, Oct. 1988 [doi>10.1016/0167-6423(88)90062-7]
• 34: Carroll Morgan, Programming from specifications (2nd ed.), Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 35: Peter Müller, Modular specification and verification of object-oriented programs, Springer-Verlag New York, Inc., New York, NY, 2002
• 36: D. A. Naumann. Verifying a secure information flow analyzer. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics TPHOLS, volume 3603 of Lecture Notes in Computer Science, pages 211--226, 2005.
• 37: E. Olderog. On the notion of expressiveness and the rule of adaptation. Theoretical Comput. Sci., 24:337--347, 1983.
• 38: M. J. Parkinson. Local reasoning for Java. Technical Report 654, University of Cambridge Computer Laboratory, Nov. 2005. The author's Ph.D. dissertation.
• 39: C. Pierik. Validation Techniques for Object-Oriented Proof Outlines. PhD thesis, Universiteit Utrecht, 2006.
• 40: A. Poetzsch-Heffter, P. Müller, and J. Schäfer. The Jive tool. http://tinyurl.com/3cke34, Apr. 2006. Checked August 2, 2006.
• 41: Peter Van Roy , Seif Haridi, Concepts, Techniques, and Models of Computer Programming, MIT Press, Cambridge, MA, 2004
• 42: N. Soundarajan and S. Fridella. Incremental reasoning for object oriented systems. In O. Owe, S. Krogdahl, and T. Lyche, editors, From Object-Orientation to Formal Methods, Essays in Memory of Ole-Johan Dahl, volume 2635 of Lecture Notes in Computer Science, pages 302--333. Springer-Verlag, 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)
      D.2.4 Software/Program Verification
          Subjects: Programming by contract; Formal methods; Correctness proofs

General Terms:
Languages, Verification

Keywords:
grey-box approach, higher order method, hoare logic, mandatory call, model program, refinement calculus, specification languages, verification