Version 3.0 (beta)
Version 3.0 (beta)
Page currently under construction !!!
Contents of this page:
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
proving the conjectures stated in the specfication,
generating proof obligations concerning the consistency
of state and operation schemas as well as their proof, and
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:
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:
The core Embedding (ZPure.thy),
the library of Z operators and their derived theory ("lib/*", in particular ZMathTool.thy),
a collection of own proof procedures (ZProofUtil.sml),
the holz-adaptor, a plugin into the ZeTa environment
providing the export functionality for Z specifications into
an internal format ("*.holz"-files),
the Method Package with the Proofobligation Manager
The compiler allowing imports of "*.holz"-files (the ZEncoder.sml)
LaTeX style files adding new features to ZeTa`s "zeta.sty" ("src/latex/*").
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:
The syntax of HOL-Z is richer than the standard syntax since 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.
HOL-Z is lexically different whenever we wanted to directly reuse Isabelle's e-mail format 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 and Davis).
With this package, we provide the following documentation:
Achim D. Brucker and Burkhart Wolff: The HOL-Z Tutorial. The most comprehensive presentation of HOL, the Z semantics in HOL, the HOL-Z system, proof techniques in HOL-Z, and its methodology. Held at the National Institute of Mathematics (NII), Tokyo, 13th of June 2008.
The generated HOL-Z documentation as pdf file and as browsable format.
A documentation of the ZeTa-System by Robert Büssow and Wolfgang Grieskamp: The Z in ZeTa. Technical University of Berlin, 2000.
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.
A collection of reference examples (such as Spivey`s BirthdayBook)
A collection of larger case-studies:
DARMA-HSD ("examples/hsd/"), a digital signature system.
See also: David Basin and Hironobu Kuruma and Kunihiko Miyazaki and
Kazuo Takaragi and Burkhart Wolff.
Verifying a signature architecture: a comparative case study. In
Formal Aspects of Computing, 2007. DOI
cvs-server ("examples/cvs-server"); a case study on modeling a
role-based access control security architecture and its refinement
of a UNIX/POSIX filesystem.
See also: Achim D. Brucker and Burkhart Wolff. A Verification
Approach for Applied System Security.
In International Journal on Software Tools for Technology Transfer
(STTT), 7 (3), pages 233-247, 2005.
Springer
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.
David Basin and Hironobu Kuruma and Kunihiko Miyazaki and Kazuo Takaragi and Burkhart Wolff. Verifying a signature architecture: a comparative case study. In Formal Aspects of Computing, 19 (1), pages 63-91, 2007.
David Basin and Hironobu Kuruma and Shin Nakajima and Burkhart Wolff. The Z Specification Language and the Proof Environment Isabelle/HOL-Z. In Computer Software - Journal of the Japanese Society for Software Science and Technology, 24 (2), pages 21-26, 2007. In Japanese.
Makarius Wenzel and Burkhart Wolff. Building Formal Method Tools in the Isabelle/Isar Framework. In TPHOLs 2007. LNCS 4732 Springer-Verlag, 2007.
David Basin and Hironobu Kuruma and Kazuo Takaragi and Burkhart Wolff. Verification of a Signature Architecture with HOL-Z. In Formal Methods 2005. LNCS 3582 Springer Verlag, 2005.
Achim D. Brucker and Burkhart Wolff. A Verification Approach for Applied System Security. In International Journal on Software Tools for Technology Transfer (STTT), 7 (3), pages 233-247, 2005.
Achim D. Brucker and Frank Rittinger and Burkhart Wolff. HOL-Z 2.0: A Proof Environment for Z-Specifications. In Journal of Universal Computer Science, 9 (2), pages 152-172, 2003.
Christoph Lüth and Einar W. Karlsen and Kolyang and Stefan Westmeier and Burkhart Wolff. HOL-Z in the UniForM-Workbench - a Case Study in Tool Integration for Z. In 11. International Conference of Z Users ZUM'98.LNCS 1493. Springer Verlag, 1998.
Kolyang and T. Santen and B. Wolff. A Structure Preserving Encoding of Z in Isabelle/HOL. In Theorem Proving in Higher Order Logics - 9th International Conference.LNCS 1125Springer Verlag, 1996.
Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL A Proof Assistant for Higher-Order Logic. LNCS 2283. 2005.
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:
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.
In some rare cases, the pretty-printing of schema decorations ("A`") is missing.
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.
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.
Burkhart Wolff: ETH Zürich
email: wolff@inf.ethz.ch
This page was lastly updated the 2008-06-16.