A theory of structured model-based specifications in Isabelle/HOL

  • Thomas Santen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1275)


We represent the concept of a class as it is proposed by object-oriented dialects of the specification language Z in Isabelle/HOL. Representing classes involves introducing different types for schemas describing states and operations, which are distinguished only by conventions in plain Z. Classes can be used in predicates to describe sets of objects. This leads us to define a trace semantics of classes, which is a basis to formally define behavioral relations between classes. The semantics of recursive classes is captured by a fixpoint construction. The representation of classes is a shallow encoding that orthogonally extends the encoding HOL-Z of plain Z in Isabelle/HOL. The extended encoding provides a well-integrated environment that is suitable to abstractly define properties of classes and to reason about concrete specifications as well.


Specification Language State Schema Class Schema Operation Schema Proof Obligation 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J.-R. Abrial. The B-Book: Assigning programs to meanings. Cambridge University Press, 1996.Google Scholar
  2. 2.
    M. Broy and S. Jähnichen, editors. KORSO: Methods, Languages, and Tools to Construct Correct Software. LNCS 1009. Springer Verlag, 1995.Google Scholar
  3. 3.
    B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.Google Scholar
  4. 4.
    R. Duke, G. Rose, and G. Smith. Object-Z: A specification language advocated for the description of standards. Computer Standards & Interfaces, 17:511–533, 1995.Google Scholar
  5. 5.
    A. Griffiths. An extended semantic foundation for Object-Z. In Asia-Pacific Software Engineering Conference, pages 194–205. Springer Verlag, 1996.Google Scholar
  6. 6.
    S. Helke, T. Neustupny, and T. Santen. Automating test case generation from Z specifications with Isabelle. In J. Bowen, M. Hinchey, and D. Till, editors, ZUM '97: The Z Formal Specification Notation, LNCS 1212, pages 52–71. Springer Verlag, 1997.Google Scholar
  7. 7.
    C. B. Jones. Systematic Software Development using VDM. Prentice Hall, 2nd edition, 1990.Google Scholar
  8. 8.
    Ed. Kazmierczak, P Kearney, O. Traynor, and Li Wand. A modular extension to Z for specification, reasoning and refinement. SVCR, Dept. of Computer Science, The University of Queensland, 1995.Google Scholar
  9. 9.
    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, LNCS 1125, pages 283–298. Springer Verlag, 1996.Google Scholar
  10. 10.
    K. Lano. Formal Object-Oriented Development. Springer Verlag, 1995.Google Scholar
  11. 11.
    K. Lano and H. Haughton, editors. Object-Oriented Specification Case Studies. Prentice Hall, 1993.Google Scholar
  12. 12.
    B. Liskov and J. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811–1841, 1994.Google Scholar
  13. 13.
    Zhaohui Luo. Program specification and data refinement in type theory. In S. Abramsky and T S. E. Maibaum, editors, Int. Joint Conference on Theory and Practice of Software Development (TAPSOFT), LNCS 493, pages 143–168, 1991.Google Scholar
  14. 14.
    B. Meyer. Reusable Software. Prentice Hall, 1994.Google Scholar
  15. 15.
    J. Nicholls. Z Notation — version 1.2. Draft ISO standard, 1995.Google Scholar
  16. 16.
    L. C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In A. Bundy, editor, Proc. 12th Conference on Automated Deduction, LNAI 814, pages 148–161. Springer Verlag, 1994.Google Scholar
  17. 17.
    L. C. Paulson. Isabelle — A Generic Theorem Prover LNCS 828. Springer Verlag, 1994.Google Scholar
  18. 18.
    E. Sekerinski. Verfeinerung in der objektorientierten Programmkonstruktion. PhD thesis, Universität Karlsruhe, 1994.Google Scholar
  19. 19.
    G. P Smith. An Object-Oriented Approach to Formal Specification. PhD thesis, University of Queensland, 1992.Google Scholar
  20. 20.
    J. M. Spivey. The Z Notation — A Reference Manual. Prentice Hall, 2nd edition, 1992.Google Scholar
  21. 21.
    S. Stepney, R. Barden, and D. Cooper, editors. Object-Orientation in Z, Workshops in Computing. Springer Verlag, 1992.Google Scholar
  22. 22.
    M. Utting and K. Whitewell. Ergo user manual. Technical Report 93–19, Software Verification Research Centre, Dept. of Computer Science, University of Queensland, 1994.Google Scholar
  23. 23.
    E W. von Henke, A. Dold, H. Rueß, D. Schwier, and M. Streckei. Construction and deduction methods for the formal development of software. In Broy and Jähnichen [2], pages 239–254.Google Scholar
  24. 24.
    M. Wenzel. Using axiomatic type classes in Isabelle. Distributed with the Isabelle system, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Thomas Santen
    • 1
  1. 1.GMD FIRSTBerlinGermany

Personalised recommendations