Programming Research Group Technical Monograph PRG-121

Stephen Brien and Andrew Martin

July 1996, 136 pages

The thesis describes the production of a large prototype proof system for Z, and a tactic language in which the proof tactics used in a wide range of systems (including the system described here) can be discussed.

The details of the construction of the tool - using the W logic for Z, and implemented in 2OBJ - are presented, along with an account of some of the proof tactics which enable W to be applied to typical proofs in Z. A case study gives examples of such proofs. Special attention is paid to soundness concerns, since it is considerably easier to check that a program such as this one produces sound proofs, than to check that each of the impenetrable proofs which it creates is indeed sound. As the first encoding of W, this helped to find bugs in the published presentation of W, and to demonstrate that W makes proof in Z tractable.

The second part of the thesis presents a tactic language, with a formal semantics (independent of any particular tool) and a set of rules for reasoning about tactics written in this language. A small set of these rules is shown to be complete for the finite (non-recursive) part of the language. Some case studies are included, as are some ideas on how this tactic language can give rise to lightweight implementations of theorem proving tools. The tool described in some detail is another theorem-prover for Z, this time based on LittleZ.