TY - JOUR AU - Brucker, Achim D. AU - Rittinger, Frank AU - Wolff, Burkhart PY - 2003 DA - 2003/02/ TI - HOL-Z 2.0: A Proof Environment for Z-Specifications JO - Journal of Universal Computer Science SP - 152 EP - 172 VL - 9 IS - 2 KW - Theorem Proving, Refinement, Z AB - 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. SN - 0948-6968 L1 - https://www.brucker.ch/bibliography/download/2003/brucker.ea-hol-z-2003.pdf UR - https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2003 UR - https://doi.org/10.3217/jucs-009-02-0152 DO - 10.3217/jucs-009-02-0152 LA - USenglish ID - brucker.ea:hol-z:2003 ER -