HOL-Z 2.0: A Proof Environment for Z-Specifications

By Achim D. Brucker, Frank Rittinger, and Burkhart Wolff.

We present a new proof environment for the specification language Z. The basis is a semantic representation of Z in a structure-preserving, shallow embedding in Isabelle/HOL. On top of the embedding, new proof support for the Z schema calculus and for proof structuring are developed. Thus, we integrate Z into a well-known and trusted theorem prover with advanced deduction technology such as higher-order rewriting, tableaux-based provers and arithmetic decision procedures. A further achievement of this work is the integration of our embedding into a new tool-chain providing a Z-oriented type checker, documentation facilities and macro support for refinement proofs; as a result, the gap has been closed between a logical embedding proven correct and a tool suited for applications of non-trivial size.

Keywords:
Theorem Proving, Refinement, Z

Please cite this work as follows:
A. D. Brucker, F. Rittinger, and B. Wolff, “HOL-Z 2.0: A proof environment for Z-specifications,” Journal of Universal Computer Science, vol. 9, no. 2, pp. 152–172, Feb. 2003, doi: 10.3217/jucs-009-02-0152. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-z-2003/

BibTeX
@Article{ brucker.ea:hol-z:2003,
  abstract     = {We present a new proof environment for the specification
                  language Z. The basis is a semantic representation of Z in a
                  structure-preserving, shallow embedding in Isabelle/HOL. On
                  top of the embedding, new proof support for the Z schema
                  calculus and for proof structuring are developed. Thus, we
                  integrate Z into a well-known and trusted theorem prover with
                  advanced deduction technology such as higher-order rewriting,
                  tableaux-based provers and arithmetic decision procedures. A
                  further achievement of this work is the integration of our
                  embedding into a new tool-chain providing a Z-oriented type
                  checker, documentation facilities and macro support for
                  refinement proofs; as a result, the gap has been closed
                  between a logical embedding proven correct and a \emph{tool}
                  suited for applications of non-trivial size.},
  author       = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
  journal      = {Journal of Universal Computer Science },
  language     = {USenglish},
  title        = {{HOL}-{Z} 2.0: {A} Proof Environment for {Z}-Specifications},
  volume       = {9},
  number       = {2},
  pages        = {152--172},
  month        = {feb},
  year         = {2003},
  keywords     = {Theorem Proving, Refinement, Z},
  copyright    = {J.UCS},
  copyrighturl = {https://www.jucs.org/jucs_9_2/hol_z_2},
  doi          = {10.3217/jucs-009-02-0152},
  issn         = {0948-6968},
  areas        = {formal methods, software},
  note         = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-hol-z-2003/}},
  pdf          = {https://logicalhacking.com/publications/brucker.ea-hol-z-2003/brucker.ea-hol-z-2003.pdf},
}