Verification of Sequential Programs: Temporal Axiomatization,
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1981
- Accession Number
- ADA111804
Entities
People
- Zohar Manna
Organizations
- Stanford University