Abstract

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

Achim D. Brucker and Frank Rittinger and 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.