Accession Number : ADA255711


Title :   Proof of Theorems in Z


Corporate Author : DEFENCE RESEARCH AGENCY MALVERN (UNITED KINGDOM)


Personal Author(s) : Smith, A


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a255711.pdf


Report Date : Mar 1992


Pagination or Media Count : 30


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.


Descriptors :   *SPECIFICATIONS , *PROGRAMMING LANGUAGES , *THEOREMS , LANGUAGE , UNITED KINGDOM , NUMBERS , PAPER


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE