Faithful mapping of model classes to mathematical structures

ABSTRACT

Abstraction techniques are indispensable for the specification and verification of functional behavior of programs. In object-oriented specification languages like JML, a powerful abstraction technique is the use of model classes, that is, classes that are only used for specification purposes and that provide object-oriented interfaces for essential mathematical concepts such as set or relation.

While the use of model classes in specifications is natural and powerful, they pose problems for verification. Program verifiers map model classes to their underlying logics. Flaws in a model class or the mapping can easily lead to unsoundness and incompleteness.

This paper proposes an approach for the faithful mapping of model classes to mathematical structures provided by the theorem prover of the program verifier at hand. Faithfulness means that a given model class semantically corresponds to the mathematical structure it is mapped to.

Our approach enables reasoning about programs specified in terms of model classes. It also helps in writing consistent and complete model-class specifications as well as in identifying and checking redundant specifications.

REFERENCES

• 1: Y. Bertot and P. Castran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, 2004.
• 2: L. Burdy, A. Requet, and J.-L. Lanet. Java applet correctness: A developer-oriented approach. In FME, volume 2805 of LNCS, pages 422--439. Springer, 2003.
• 3: J. Charles. Adding Native Specifications to JML. In Formal Techniques for Java-like Programs, 2006.
• 4: Yoonsik Cheon , Gary Leavens , Murali Sitaraman , Stephen Edwards, Model variables: cleanly supporting abstraction in design by contract: Research Articles, Software—Practice & Experience, v.35 n.6, p.583-599, May 2005 [doi>10.1002/spe.v35:6]
• 5: A. Darvas and K. R. M. Leino. Practical reasoning about invocations and implementations of pure methods. In FASE, volume 4422 of LNCS, pages 336--351. Springer, 2007.
• 6: A. Darvas and P. Müller. Reasoning About Method Calls in Interface Specifications. JOT, 5(5):59--85, 2006.
• 7: J.-C. Filliâtre, T. Hubert, and C. Marché. The Caduceus verification tool for C programs. Tutorial and Reference Manual. 2007.
• 8: J.-C. Filliâtre and C. Marché. Multi-prover verification of C programs. In ICFEM, volume 3308 of LNCS, pages 15--29. Springer, 2004.
• 9: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, ACM SIGPLAN Notices, v.37 n.5, May 2002
• 10: John V. Guttag , James J. Horning, Larch: languages and tools for formal specification, Springer-Verlag New York, Inc., New York, NY, 1993
• 11: Thierry Hubert , Claude Marche, A case study of C source code verification: the Schorr-Waite algorithm, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.190-199, September 07-09, 2005 [doi>10.1109/SEFM.2005.1]
• 12: B. Jacobs and F. Piessens. Verification of programs with inspector methods. In Formal Techniques for Java-like Programs, 2006.
• 13: Gary T. Leavens , Yoonsik Cheon , Curtis Clifton , Clyde Ruby , David R. Cok, How the design of JML accommodates both runtime assertion checking and formal verification, Science of Computer Programming, v.55 n.1-3, p.185-208, March 2005 [doi>10.1016/j.scico.2004.05.015]
• 14: 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]
• 15: G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, P. Müller, and J. Kiniry. JML Reference Manual. Iowa State University, Last revised February 2007.
• 16: J. Meyer, P. Müller, and A. Poetzsch-Heffter. The JIVE system---implementation description. 2000.
• 17: M. Miragliotta. Specification model library for the interactive program prover JIVE. ETH Zurich, Semester Thesis, 2004.
• 18: T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL -- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
• 19: T. Nipkow, L. C. Paulson, and M. Wenzel. Theory HOL/Set from "The Isabelle Library". isabelle.in.tum.de/library/HOL/Set.html, 2005.
• 20: B. Schoeller. Strengthening Eiffel contracts using models. In Formal Aspects of Component Software, 2003.
• 21: B. Schoeller, T. Widmer, and B. Meyer. Making specifications complete through models. In Architecting Systems with Trustworthy Components, volume 3938 of LNCS. Springer, 2006.
• 22: N. Shankar, S. Owre, and J. M. Rushby. A Tutorial on Specification and Verification Using PVS (Beta Release). Technical report, Computer Science Laboratory, SRI International, March 1993.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Programming by contract; Formal methods

General Terms:
Verification

Keywords:
abstraction, isomorphism, java modeling language, model classes, specification, verification