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.
Keywords:
Categories: ,
Documents: (full text as PDF file)
Please cite this article as follows:
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, and Burkhart Wolff.
HOL-Z 2.0: A Proof Environment for Z-Specifications.
In FM-TOOLS 2002, pages 33-38, 2002. Available as Technical Report, University Augsburg, number 2002-11.
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (
| 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.}, | |
| address | = | {Augsburg}, | |
| author | = | {Achim D. Brucker and Stefan Friedrich and Frank Rittinger and Burkhart Wolff}, | |
| booktitle | = | {FM-TOOLS 2002}, | |
| editor | = | {Dominik Haneberg and Gerhard Schellhorn and Wolfgang Reif}, | |
| language | = | {USenglish}, | |
| month | = | {jul}, | |
| note | = | {Available as Technical Report, University Augsburg, number 2002--11.}, | |
| organization | = | {University Augsburg}, | |
| pages | = | {33--38}, | |
| = | {https://www.brucker.ch/bibliography/download/2002/brucker.ea-hol-z-2002.pdf}, | ||
| title | = | {{HOL}-{Z} 2.0: {A} Proof Environment for {Z}-Specifications}, | |
| url | = | {https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2002}, | |
| year | = | {2002}, |