@Article{ brucker.ea:hol-z:2003,
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},
journal = {Journal of Universal Computer Science},
language = {USenglish},
title = {{HOL}-{Z} 2.0: {A} Proof Environment for
{Z}-Specifications},
volume = {9},
number = {2},
pages = {152--172},
month = feb,
year = {2003},
pdf = {https://www.brucker.ch/bibliography/download/2003/brucker.ea-hol-z-2003.pdf},
keywords = {Theorem Proving, Refinement, Z},
copyright = {J.UCS},
copyrighturl = {http://www.jucs.org/jucs_9_2/hol_z_2},
categories = {holz},
doi = {10.3217/jucs-009-02-0152},
issn = {0948-6968},
classification= {journal},
areas = {formal methods, software},
public = {yes},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2003}
}