Le Système HOL-Z - The HOL-Z System
Person in charge :
WOLFF Burkhart
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 typechecked 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.
More information: http://www.brucker.ch/projects/hol-z/
- Licence :
GPL
Research activities
Formalisation of (Specification and Programming) Languages in Proof Assistants
Members
WOLFF Burkhart
Group
Verification of Algorithms, Languages and Systems
