A project to develop an inductive proof assistant for Z integrating classical and rewrite strategies

Z is a formal specification language 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 propose the development of such a reasoning assistant for Z. Utilising the concept of "ordered covering", our proposed approach will combine aspects of both the classical and rewrite-based approaches to proof by induction. In particular, it will include the classical induction "on variables " and use of heuristics, and the rewrite-based induction "on subterms " and unification for generation of induction cases. In this way, we will not only be developing an inductive reasoner for Z but will be furthering our understanding of the automation of proof by induction. To ensure that our reasoning principles and strategies are appropriate for Z, we propose to implement them in CADiZ, an interactive reasoning tool for Z developed at the University of York. We will evaluate the utility of the resulting system by attempting to construct a broad range of proofs, including some of practical importance to computer security, safety-critical systems and compiler correctness