
Accession Number : ADA111804
Title : Verification of Sequential Programs: Temporal Axiomatization,
Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
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