Object-oriented verification based on record subtyping in Higher-Order Logic
We show how extensible records with structural subtyping can be represented directly in Higher-Order Logic (HOL). Exploiting some specific properties of HOL, this encoding turns out to be extremely simple. In particular, structural subtyping is subsumed by naive parametric polymorphism, while overridable generic functions may be based on overloading. Taking HOL plus extensible records as a starting point, we then set out to build an environment for object-oriented specification and verification (HOOL). This framework offers several well-known concepts like classes, objects, methods and late-binding. All of this is achieved by very simple means within HOL.
KeywordsTheorem Prove Correctness Proof Record Type Concrete Syntax Colour Point
Unable to display preview. Download preview PDF.
- 1.P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986.Google Scholar
- 2.A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, pages 56–68, 1940.Google Scholar
- 3.M. J. C. Gordon and T. F. Melham (editors). Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.Google Scholar
- 4.U. Hensel, M. Huisman, B. Jacobs, and H. Tews. Reasoning about classes in object-oriented languages: Logical models and tools. In Proceedings of ESOP/ETAPS, volume 1381 of Lecture Notes in Computer Science. Springer-Verlag, 1998.Google Scholar
- 5.M. Hofmann, W. Naraschewski, M. Steffen, and T. Stroup. Inheritance of proofs. Theory and Practice of Object Systems, Special Issue on Third Workshop on Foundations of Object-Oriented Languages (FOOL 3), 4(1):51–69, 1998.Google Scholar
- 6.L. Lamport and L. C. Paulson. Should your specification language be typed? Technical Report 425, University of Cambridge Computer Laboratory, 1997.Google Scholar
- 8.W. Naraschewski. Object-Oriented Proof Principles using the Proof-Assistant Lego. Diplomarbeit, UniversitÄt Erlangen, 1996.Google Scholar
- 9.W. Naraschewski. Towards an object-oriented progification language. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, volume 1275 of Lecture Notes in Computer Science, pages 215–230. Springer-Verlag, 1997.Google Scholar
- 10.L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.Google Scholar
- 12.A. Pitts. The HOL logic. In Gordon and Melham , pages 191–232.Google Scholar
- 13.M. Wenzel. Type classes and overloading in higher-order logic. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, volume 1275 of Lecture Notes in Computer Science, pages 307–322. Springer-Verlag, 1997.Google Scholar