A TUTORIAL ON PROOF IN STANDARD Z
Stephm Brien and Andrew Martin
Abstract
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 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 specifications.
Institution
OUCL
Month
February
Number
PRG120
Pages
66
Year
1996