
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/
@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
\LaTeX-based front
Z on top of Isabelle/HOL. It comprises a
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.. \url{https://logicalhacking.com/publications/brucker.ea-hol-z-2002/}},
Author copy: obsoletedby = {brucker.ea:hol-z:2003},
pdf = {https://logicalhacking.com/publications/brucker.ea-hol-z-2002/brucker.ea-hol-z-2002.pdf},
}