Proof of Theorems in Z
Abstract
This paper is concerned with user aspects of proof in the specification language Z. A number of techniques for proving theorems in Z are presented. Some of the techniques are not new, being drawn from the area of general mathematical theorem proving, but are brought together in one place and applied specifically to Z. The techniques have been written so that they can be understood and applied by a person carrying out a pen and paper proof. Some of the techniques may be automated, and would result in a proof tool tailored to the needs of the user; currently a user has to tailor a proof to fit a tool.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 1992
- Accession Number
- ADA255711
Entities
People
- A. Smith