HOL-Z 2.0: A Proof Environment for Z-Specifications
Achim D. Brucker, Frank Rittinger und 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.
Schlüsselwörter: Theorem Proving, Refinement, Z
Kategorien: ,
Dokumente: (Artikel als PDF Datei)
Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker, Frank Rittinger und Burkhart Wolff.
HOL-Z 2.0: A Proof Environment for Z-Specifications.
In Journal of Universal Computer Science, 9 (2), pages 152-172, 2003.
Schlüsselwörter: Theorem Proving, Refinement, Z
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.3217/jucs-009-02-0152) (J.UCS) (
)
| 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}, | |
| copyright | = | {J.UCS}, | |
| copyrighturl | = | {http://www.jucs.org/jucs_9_2/hol_z_2}, | |
| doi | = | {10.3217/jucs-009-02-0152}, | |
| issn | = | {0948-6968}, | |
| journal | = | {Journal of Universal Computer Science}, | |
| keywords | = | {Theorem Proving, Refinement, Z}, | |
| language | = | {USenglish}, | |
| month | = | {feb}, | |
| number | = | {2}, | |
| pages | = | {152--172}, | |
| = | {https://www.brucker.ch/bibliography/download/2003/brucker.ea-hol-z-2003.pdf}, | ||
| title | = | {{HOL}-{Z} 2.0: {A} Proof Environment for {Z}-Specifications}, | |
| url | = | {https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2003}, | |
| volume | = | {9}, | |
| year | = | {2003}, |