Advertisement

Object-oriented verification based on record subtyping in Higher-Order Logic

  • Wolfgang Naraschewski
  • Markus Wenzel
Refereed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1479)

Abstract

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.

Keywords

Theorem Prove Correctness Proof Record Type Concrete Syntax Colour Point 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986.Google Scholar
  2. 2.
    A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, pages 56–68, 1940.Google Scholar
  3. 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. 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. 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. 6.
    L. Lamport and L. C. Paulson. Should your specification language be typed? Technical Report 425, University of Cambridge Computer Laboratory, 1997.Google Scholar
  7. 7.
    J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. ACM Trans. Prog. Lang. Syst., 10(3):470–502, July 1988.CrossRefGoogle Scholar
  8. 8.
    W. Naraschewski. Object-Oriented Proof Principles using the Proof-Assistant Lego. Diplomarbeit, UniversitÄt Erlangen, 1996.Google Scholar
  9. 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. 10.
    L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.Google Scholar
  11. 11.
    B. C. Pierce and D. N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–247, 1994.zbMATHCrossRefGoogle Scholar
  12. 12.
    A. Pitts. The HOL logic. In Gordon and Melham [3], pages 191–232.Google Scholar
  13. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Wolfgang Naraschewski
    • 1
  • Markus Wenzel
    • 1
  1. 1.Institut für InformatikTechnische UniversitÄt MünchenMünchenGermany

Personalised recommendations