@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} }