Programming Research Group Technical Monograph PRG-120

Stephen Brien and Andrew Martin

February 1996, 70 pages

In these notes we present material designed to support an explanation of how to conduct proofs using the deductive system presented in the draft Z Standard. This is, of course one of the possible deductive systems for Z. We aim to present an account of the various components of the deductive system, showing how they are used together, and how they permit the formal proof of theorems involving sizeable Z specifications.

The method of proof is supported by JigsaW, a theorem proving assistant into which the deductive system of standard Z has been incorporated. We further aim to show how JigsaW's support of the tactic langauge Angel allows proofs to be defined in a more general and reusable way.

An appendix gives the relevant sections of the current draft standard. We do not aim to explain every rule, but merely enough to allow the reader to read, understand, and use the standard's deductive system. Our work in logics for Z has been greatly helped by collaboration with Jim Woodcock, and review from other members of the Z Standards Panel. In particular we have benefited from the work of Jones (1990) and Harwood (1990).

Most of the material used here is derived from the project Models, Algebra, and Mechanical Support in Z, funded by EPSRC grant number GR/J46630.