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

Achim D. Brucker (Albert-Ludwigs-University Freiburg, Germany)

Frank Rittinger (Albert-Ludwigs-University Freiburg, Germany)

Burkhart Wolff (Albert-Ludwigs-University Freiburg, Germany)

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 tool suited for applications of nontrivial size.

Keywords: Z, refinement, theorem proving

Categories: D.2.1, D.2.4, F.3.1, F.4.1