Accession Number:

ADA255711

Title:

Proof of Theorems in Z

Descriptive Note:

Corporate Author:

DEFENCE RESEARCH AGENCY MALVERN (UNITED KINGDOM)

Personal Author(s):

Report Date:

1992-03-01

Pagination or Media Count:

30.0

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE