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

Achim D. Brucker, Stefan Friedrich, Frank Rittinger und Burkhart Wolff

Cover for brucker.ea:hol-z:2002.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.

Schlüsselwörter:
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for brucker.ea:hol-z:2002.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker, Stefan Friedrich, Frank Rittinger und 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.
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@InCollection{ brucker.ea:hol-z:2002,
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},
pdf = {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},
}