Version 2.1.1

Contents of this page:

• What is HOL-Z?
• Documentation
• Current Release
• Installation
• Contributors
• Contact Address

What is HOL-Z 2.1.1?

HOL-Z is a proof environment for Z and HOL specifications based on ZeTa on the one hand and the generic theorem prover Isabelle (Version 98-0) on the other. ZeTa is essentially used as a type-checker for literate specifications in Z, that can be integrated into XEMACS as a combined editing and type-checking frontend. ZeTa has been extended by a plugin, that converts Z sections into a new format (*.holz) that can be loaded alternatively to Isabelles standard theory files (*.thy-files). Thus, theory contexts can be created in which theorem proving for specifications of realistic size can be realized.

On the Isabelle side, Z has been represented in a structure preserving embedding of Z into the higher-order logic (HOL) instance of Isabelle. Technically speaking, HOL-Z is a shallow embedding. 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 three parts:

• A LaTeX-setup supporting literate specification and proof obligation generation.
• A setup for ZeTa, that can be integrated into XEmacs, and a plugin to produce Isabelle input.
• The conservative embedding of Z into Isabelle/HOL itself.

The LaTeX setup contains an own LaTeX-style file holz.sty which provides mainly a new command zrefines for refinement. This environment generates automatically refinement conditions for further processing with ZeTa and proof obligations for Isabelle/HOL-Z. For further details, please see the holz-manual which can after a succesfull installation of HOL-Z 2.1.1 can be found in the directory lib/texmf/doc/holz.

The ZeTa setup uses the ZeTa environment to load LaTex-based Z-specifications, type check them and with the help of a new adaptor, export them into files which can be loaded by Isabelle. You only have one specification document with text and formal notation which can be nicely type set. For detailed documentation on the HOL-Z-adaptor for ZeTa and its interaction with Isabelle, please have a look at its documentation.

• An Isabelle theory ZPure (containing the e-mail format of Z roughly along the Z Standard )
• A collection of extensions of the Isabelle/HOL-standard (contrib)
• A collection of library theories, the mathematical toolkit (lib)
• A setup of Isabelles loader for e-mail format based Z-Sections (in *.thy-Files)
• A collection of tactics to support working with Z (ZProofUtils, prover)
• A loader and converter of ZeTa-generated *.holz files ("use_holz")
  WE ADVISE TO USE THIS MECHANISM FOR LARGER SPECIFICATIONS.

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 syntactic front-end --- based on previous LaTeX styles that influenced the standard --- is inherited from ZeTa and conforms to a large degree to the standard (see The Z in ZeTa). 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. This is mainly for the following reasons:

• The syntax of HOL-Z is too rich because it includes standard HOL theories. Since we are interested in real theorem proving, there is no point to forbid the use of existing extra libraries and proof support.
• We do not support all constructs of Z, mainly because Z provides many syntactic alternatives that are tedious to support and, worse, hamper theorem proving.
• HOL-Z is syntactically different whenever we wanted to directly reuse Isabelle's lexical conventions, HOL-library-conventions, etc. In rare cases, we changed Z syntax to enhance Isabelle's parsing machinery. For example, items in the declaration part of a schema must be separated with a ";" from each other, and schema declarations must be enclosed as strings("abc"), any backslash \ has to be preceeded by a quoting one (an inhertitance from ML) etc.
• HOL-Z is designed to be a mixed logical language; this allows for logical statements over formulas that do not belong to the Z standard, but arise naturally during theorem proving --- such mixed statements were even used in canonical textbooks on Z (like Using Z by Woodcock abd Davis).

Documentation

• A revised version of the paper A Structure Preserving Encoding of Z in Isabelle/HOL which has originally been published at TPHOLs96.
• An journal paper describing HOL-Z 2.0 published in the Journal of Universal Computer Science.
• An extended abstract describing HOL-Z 2.0 published in the FMTOOLS2002.
• Miscellaneous papers.
• Online documentation for implementation details.
• The Isabelle generated HTML-documentation for HOL-Z theories.
• A collection of reference examples (bbook in e-mail format and in LaTeX format (examples/zeta/bbook)).
• A collection of larger case-studies:
  • cvs-server (examples/zeta/cvs-server); a case study on modeling a role-based access control security architecture and its refinement of a UNIX/POSIX filesystem.
  • corba-sec (examples/zeta/corba-sec); a case study on the CORBA security service.
  • leplas (examples/zeta/leplas); a case study on a class scheduling system.

Current Release

HOL-Z 2.1.1 is Free Software in the sense of the GPL. The current release (dated: 2004-01-30) has version number 2.1.1.

• User-defined Generic Schemas are not supported.
• Free Types:  variants with arguments are not supported.
  Work-around: For non-recursive cases, the injections into sums Inl or Inr can be used (this is an extension of the Z standard; see example cvs-server). Otherwise use HOL's own datatype mechanism.
• E-mail format: The Z selection-notation "A.x" where A is a schema and x an identifier of A do not work always, since HOL-Z represents bindings by products and uses hence a weaker type system.
  Work-around: avoid such constructions in the e-mail format or provide the necessary projections by hand
• Not all schema decorations and schema calculus operations are supported.
• The pretty printer is quite buggy --- in particular for mixed Z and HOL fomulas, situations emerge where pretty prints are misleading or simply wrong.
  Work-around: use "show_full_sem:=true" to shut up most pretty printing.
• E-mail format: Error messages are sometimes cryptic and arcane. In particular, take care that names in Z specifications are disjoint from names in HOL; for example, it is a bad idea to name a schema trans since there is a function with the same name in HOL. Isabelles own type-checker using the compiled ZeTa-output will not be able to resolve the name conflict

Installation

After unpacking the HOL-Z sources (version 2.1.1) you find a file INSTALL. It contains the details about the installation.

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 Neustupny and Carsten Sühl of the GMD/First made substantial contributions. Boris Witz 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.

Following the general conventions of Free Software, all authors can be found in the AUTHORS file of the distribution.

Contact Address

• Burkhart Wolff: University of Freiburg, 79110 Freiburg i. Br., Germany
  email: wolff@informatik.uni-freiburg.de