Advertisement

Encoding Object-Z in Isabelle/HOL

  • Graeme Smith
  • Florian Kammüller
  • Thomas Santen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)

Abstract

In this paper, we present a formalisation of the reference semantics of Object-Z in the higher-order logic (HOL) instantiation of the generic theorem prover Isabelle, Isabelle/HOL. This formalisation has the effect of both clarifying the semantics and providing the basis for a theorem prover for Object-Z. The work builds on an earlier encoding of a value semantics for object-oriented Z in Isabelle/HOL and a denotational semantics of Object-Z based on separating the internal and external effects of class methods.

Keywords

Object-Z reference semantics higher-order logic Isabelle 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    H. Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science, Vol. 2. Oxford University Press, 1992.Google Scholar
  2. 2.
    J. Bowen and M. Gordon. A shallow embedding of Z in HOL. Information and Software Technology, 37(5–6):269–276, 1995.CrossRefGoogle 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.
    A. Griffiths. A Formal Semantics to Support Modular Reasoning in Object-Z. PhD thesis, University of Queensland, 1997.Google Scholar
  5. 5.
    A. Griffiths. Object-oriented operations have two parts. In D.J. Duke and A.S. Evans, editors, 2nd BCS-FACS Northern Formal Methods Workshop, Electronic Workshops in Computing. Springer-Verlag, 1997.Google Scholar
  6. 6.
    F. Kammüller. Modular Reasoning in Isabelle. PhD thesis, Computer Laboratory, University of Cambridge, 1999. Technical Report 470.Google Scholar
  7. 7.
    Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/ HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics (TPHOLs 96), volume 1125 of Lecture Notes in Computer Science, pages 283–298. Springer-Verlag, 1996.Google Scholar
  8. 8.
    L.C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.zbMATHGoogle Scholar
  9. 9.
    T. Santen. A theory of structured model-based specifications in Isabelle/HOL. In E.L. Gunter and A. Felty, editors, Theorem Proving in Higher-Order Logics (TPHOLs 97), volume 1275 of Lecture Notes in Computer Science, pages 243–258. Springer-Verlag, 1997.CrossRefGoogle Scholar
  10. 10.
    T. Santen. On the semantic relation of Z and HOL. In J. Bowen and A. Fett, editors, ZUM’98: The Z Formal Specification Notation, LNCS 1493, pages 96–115. Springer-Verlag, 1998.CrossRefGoogle Scholar
  11. 11.
    T. Santen. Isomorphisms-a link between the shallow and the deep. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, editors, Theorem Proving in Higher Order Logics, LNCS 1690, pages 37–54. Springer-Verlag, 1999.CrossRefGoogle Scholar
  12. 12.
    T. Santen. A Mechanized Logical Model of Z and Object-Oriented Specification. Shaker-Verlag, 2000. Dissertation, Fachbereich Informatik, Technische Universität Berlin, (1999).Google Scholar
  13. 13.
    G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.Google Scholar
  14. 14.
    G. Smith. Recursive schema definitions in Object-Z. In A. Galloway J. Bowen, S. Dunne and S. King, editors, International Conference of B and Z Users (ZB 2000), volume 1878 of Lecture Notes in Computer Science, pages 42–58. Springer-Verlag, 2000.Google Scholar
  15. 15.
    H. Tej and B. Wolff. A corrected failure-divergence model for CSP in Isabelle/HOL. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, Formal Methods Europe (FME 97), volume 1313 of Lecture Notes in Computer Science, pages 318–337. Springer-Verlag, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Graeme Smith
    • 1
  • Florian Kammüller
    • 2
  • Thomas Santen
    • 2
  1. 1.Software Verification Research CentreUniversity of QueenslandAustralia
  2. 2.Technische Universität BerlinBerlinGermany

Personalised recommendations