Abstract:

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

Achim D. Brucker and Stefan Friedrich and Frank Rittinger and Burkhart Wolff


We present a proof environment for the specification language Z on top of Isabelle/HOL. It comprises a 
LaTeX-based front end (including the integrated type-checker ZETA), generic facilities to generate proof 
obligations and improved proof support for the logical embedding HOL-Z, namely for the schema-calculus 
and structural Z proofs.