Z is a formal specification language based upon Zermelo-Fraenkel set theory that is extensively used in both
academia and industry. Several tools have been developed for reasoning about Z specifications, but they all lack
substantial facilities for inductive reasoning. We are developing such a reasoning assistant for
Standard Z. Utilising the concept of "ordered
covering", our approach combines aspects of both the classical and rewrite-based approaches to proof by induction.
In this way, we not only develop an inductive reasoner for Z but further our understanding of the automation of
proof by induction. To ensure that our reasoning principles and strategies are appropriate for Z, we implement
them in CADiZ, an interactive reasoning tool for Z
developed at the University of York.
Objectives
To formulate new principles of induction and strategies for inductive case generation that combine aspects
of the classical and rewrite-based approaches. We evaluate this by characterising the extent to which the
new principles and strategies subsume previous ones.
To tailor these principles and strategies to the Z specification language and implement them as a proof
assistant in CADiZ. We evaluate the utility of the resulting system by constructing a broad range of proofs,
including some of practical importance to computer security, safety-critical systems and compiler correctness.
This is EPSRC project L31104. Its members are Alan Frisch,
David Duffy, Ian Toyn and Sam Valentine.
Example proofs may be found in examples. A collection
of tactics used in the proofs may be found in tactics.
References
Below are a project summary and project-related papers written by members of the group. Where electronic versions
are available, the format of files is indicated by the usual filename extensions when the paper is selected. For
example, file.ps.gz is gzipped postscript.
Alan M. Frisch, David A. Duffy, and Ian Toyn.
A Project to Develop an Inductive Proof Assistant for Z
Integrating Classical and Rewrite Strategies.
Case for support, 1997.
David A. Duffy, Alan M. Frisch, and Ian Toyn.
Proof by induction: Bridging the Gap between Proof Theory and
Practical Automated Proof Systems.
In Michael Fisher, editor, Working Notes, 1997 AISB Workshop on Automated Reasoning:
Bridging the Gap between Theory and Practice, Manchester, April 1997.
David A. Duffy.
Partial Functions in the Z Specification Language.
In M. Kerber, editor, CADE-15 Workshop on Mechanisation of Partial Functions,
Lindau, Germany, July 1998.
Ian Toyn.
A Tactic Language for Reasoning about Z Specifications.
In proceedings 3rd Northern Formal Methods Workshop, Ilkley, Sept 1998,
published electronically by Springer in eWiC.
David A. Duffy.
Lemma-Generation and Rippling Tactics in the CADiZ Proof System.
Technical Report YCS-2000-325, Department of Computer Science, University of York, 2000.
Alan M. Frisch, David A. Duffy, Ian Toyn, and Samuel H. Valentine.
A Project to Develop an Inductive Proof Assistant for Z Integrating
Classical and Rewrite Strategies. Final Report, 2000.