HOL-Z
Version 3.0 (beta)

Page currently under construction !!!

Welcome to the Isabelle/HOL-Z home page!


Contents of this page:


What is Isabelle/HOL-Z 3.0 (beta)?

HOL-Z is a proof environment for Z built as plug-in of the generic theorem prover Isabelle/HOL (Version 2005). It allows for importing Z specifications written in LaTeX and type-checked by the Java-based ZeTa-System. HOL-Z then allows for the formal analysis of such specifications, i.e. by

  1. proving the conjectures stated in the specfication,

  2. generating proof obligations concerning the consistency
    of state and operation schemas as well as their proof, and

  3. generating proof obligations resulting from refinement
    statements for functional and data refinement (cf. Spivey`s The Z Reference Manual).

Proof documents containing lemmas, analytical statements, proofs and global checks were written in an extension of the Isabelle/ISAR proof language and can be edited with the emacs-based ProofGeneral 3.6 interface. Here is a screenshot of HOL-Z 3.0 running under ProofGeneral:

HOL-Z Screenshot

There is also a batchmode (in form of the standard Isabelle system command "isatool make") that can be used to check the overall consistency of a collection of HOL-Z documents ("*.thy"-files) and to generate LaTeX documentation from them. Here is a standard example.

Technically, HOL-Z consists of a structure preserving shallow embedding of Z into the higher-order logic (HOL). On this embedding, libraries for the "Mathematical Toolkit" of Z were added as well as configuations of Isabelles standard proof procedures. Furthermore, there are as Z specific proof methods mostly to support the Z schema calculus as well as Z type constraints. Finally, there is a compiler inside the import-function "use_holz" that allows for the import of ZeTa output.

Together with its ability to preserve the structure of large specifications, this has the advantage that inferences in HOL-Z were based on derived rules that were controlled by tactical programs. Thus, HOL-Z can be extended in a logically consistent and safe way. However, HOL-Z cannot be used for meta-theoretic reasoning over Z. HOL-Z essentially consists of six parts:

Of course, all these features are add-ons to the Isabelle/HOL and ProofGeneral Interface and its mechanisms and features.

The essential part of the embedding is its representation in the set theory of higher-order logic. The semantic representation conforms to the Z Draft ISO Standard, because the semantics of Z defines a typed set theory while using the untyped set theory ZF as meta-language. The representation in set theory can be found in the Isabelle theory ZMathTool.

The syntax for Z comes from two sources: a LaTeX-format and the standards e-mail format. ZeTa input is written in a LaTeX variant described in the ZeTa documentation (see The Z in ZeTa). For most operators, a translation of these can be also be used in the ".thy" files edited and verified in HOL-Z. The syntactic representation of the e-mail format aims to conform to the Z Draft ISO Standard, but achieves this goal to a far lesser extent. All operators can be represented in this format in the ".thy" files. The details have to be drawn from the theories and the system documentation generated from them.

There are a number of limitations:


Documentation

With this package, we provide the following documentation:


Bibliography


Download

HOL-Z is Free Software in the sense of the GPL.

It requires Isabelle/HOL 2005 and ZeTa, which have to be installed before. Here are the a sources of HOL-Z 3.0 (beta).

The previous version is sources (version 2.1.1) (dated: 2004-01-30).

Even the current release has a number of quite substantial limitions. These are in particular:


Installation

HOL-Z requires Isabelle/HOL 2005 and ZeTa. After unpacking the HOL-Z sources (version 3.0 beta) you find a file INSTALL. It contains further details. The installation procedure differes substantially from previous versions and is now conform to Isabelle`s standard mechanisms.


Release History and Contributors

HOL-Z Version 1.0 (and variations thereof) have been developped by Kolyang, Thomas Santen and Burkhart Wolff; HOL-Z 1.0 was developped jointly at the BISS at the University Bremen and the GMD/First,Berlin. Steffen Helke, Thomas Neustruppy and Carsten Suhl of the GMD/First made substantial contributions. Boris Wirtz of the University Oldenburg made a larger Case Study (a protocol specification) on the basis of HOL-Z 1.0 that lead to substantial improvements.

The major release 2.0 was develped by Achim D. Brucker, Frank Rittinger, and Burkhart Wolff. The Authors of HOL-Z Version 2.1.1 are Achim D. Brucker, Harald Hiss and Burkhart Wolff.

The major release HOL-Z 3.0 was mostly developed by Achim D. Brucker, Lukas Brügger, and Burkhart Wolff.

Contact Address


This page was lastly updated the 2008-06-16.