Tutorial on Proof in Standard Z. Z User Meeting '95. Held in Limerick, Ireland onSeptember 5, 1995

摘要

In these notes we presented material designed to support an explanation of how toconduct proofs using the deductive system presented in the draft Z Standard. This is, of course one of several 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 specification. (Copyright (c) 1996 Stephen Brien and Andrew Martin.)