Accession Number : ADA111804

Title :   Verification of Sequential Programs: Temporal Axiomatization,


Personal Author(s) : Manna,Zohar

PDF Url : ADA111804

Report Date : Sep 1981

Pagination or Media Count : 46

Abstract : This is one in a series of reports describing the application of temporal logic to the specification and verification of computer programs. Earlier reports, introduced temporal logic as a tool for reasoning about concurrent computer programs and specifying their properties (MP1) and presented proof principles for establishing these properties (MP2). This report focuses on deterministic, sequential programs. Presented is a proof system in which properties of such programs, expressed as temporal formulas, can be proved formally. This proof system consists of three parts: a general part elaborating the properties of temporal logic, a domain part giving an axiomatic description of the data domain, and a program part giving an axiomatic description of the program under consideration. The use of the proof system is illustrated through the presentation of two alternative formal proofs of the total correctness of a simple program.

Descriptors :   *Computer program verification, *Computer logic, *Specifications, Programming languages, Sequential analysis, Determinants(Mathematics), Equations

Subject Categories : Statistics and Probability
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE