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

  1. 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.
  2. 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.

[FDT97]
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.
[DFT97a]
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.
[DFT97b]
David A. Duffy, Alan M. Frisch, and Ian Toyn. Free-Type Induction in CADiZ. Unpublished, 1997.
[Duffy98a]
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.
[Duffy98b]
David A. Duffy. On Partial-Function Application in Z. In proceedings 3rd Northern Formal Methods Workshop, Ilkley, Sept 1998, published electronically by Springer in eWiC. ©Springer-Verlag
[Toyn98a]
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.
[Toyn98b]
Ian Toyn. Innovations in the Notation of Standard Z. Proceedings 11th Z User Meeting, Berlin, Sept 1998.
[Duffy99]
David A. Duffy. Partial Functions in a Simply-Typed Set-Theoretic Language. Submitted, July 1999.
[Duffy00a]
David A. Duffy. A Generalised Coverset Induction Principle. Technical Report YCS-2000-323, Department of Computer Science, University of York, 2000.
[Duffy00b]
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.
[TVD00]
Ian Toyn, Samuel H. Valentine, and David A. Duffy. On Mutually Recursive Free Types in Z. Proceedings International Conference of Z and B Users, ZB2000, LNCS. Springer, 2000. ©Springer-Verlag.
[DT00]
D Duffy and Ian Toyn. Reasoning Inductively about Z Specifications via Unification. Proceedings International Conference of Z and B Users, ZB2000, LNCS. Springer, 2000. ©Springer-Verlag
[DG00]
D Duffy and J. Giesl. Closure Induction in a Z-like Language. Proceedings International Conference of Z and B Users, ZB2000, LNCS. Springer, 2000. ©Springer-Verlag
[Valentine00]
Samuel H. Valentine Formal Studies of Structural Induction. To appear as Technical Report, Department of Computer Science, University of York, 2000.
[FDTV00]
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.