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

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

We present a proof environment for the specification language Z on top of Isabelle/HOL. It comprises a LaTeX-based front end (including the integrated type-checker ZETA), generic facilities to generate proof obligations and improved proof support for the logical embedding HOL-Z, namely for the schema-calculus and structural Z proofs.

Obsoleted by:
This publication has been obsoleted by the following publication:
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/

Please cite this work as follows:
A. D. Brucker, S. Friedrich, F. Rittinger, and B. Wolff, “HOL-Z 2.0: A proof environment for Z-specifications,” in FM-TOOLS 2002, D. Haneberg, G. Schellhorn, and W. Reif, Eds. Augsburg: University Augsburg, 2002, pp. 33–38. Available as Technical Report, University Augsburg, number 2002–11.. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-z-2002/

BibTeX
@InCollection{ brucker.ea:hol-z:2002,
  author       = {Achim D. Brucker and Stefan Friedrich and Frank Rittinger and
                  Burkhart Wolff},
  title        = {{HOL}-{Z} 2.0: {A} Proof Environment for {Z}-Specifications},
  editor       = {Dominik Haneberg and Gerhard Schellhorn and Wolfgang Reif},
  booktitle    = {FM-TOOLS 2002},
  year         = {2002},
  pages        = {33--38},
  month        = {jul},
  organization = {University Augsburg},
  address      = {Augsburg},
  language     = {USenglish},
  abstract     = {We present a proof environment for the specification language
                  Z on top of Isabelle/HOL. It comprises a \LaTeX-based front
                  end (including the integrated type-checker ZETA), generic
                  facilities to generate proof obligations and improved proof
                  support for the logical embedding HOL-Z, namely for the
                  schema-calculus and structural Z proofs.},
  areas        = {formal methods, software},
  note         = {Available as Technical Report, University Augsburg, number
                  2002--11.. 
                  Author copy: \url{https://logicalhacking.com/publications/brucker.ea-hol-z-2002/}},
  obsoletedby  = {brucker.ea:hol-z:2003},
  pdf          = {https://logicalhacking.com/publications/brucker.ea-hol-z-2002/brucker.ea-hol-z-2002.pdf},
}