Axiomatic Approach to Total Correctness of Programs
Abstract
The authors present an axiomatic approach which enables one to prove by formal methods that his program is totally correct (i.e., it terminates and is logically correct -- does what it is supposed to do). The approach is similar to Hoare's approach for proving that a program is partially correct (i. e., that whenever it terminates it produces correct results). The extension to Hoare's method lies in the possibility of proving correctness and termination at once, and in the enlarged scope of properties that can be proved by it.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1973
- Accession Number
- AD0767335
Entities
People
- Amir Pnueli
- Zohar Manna
Organizations
- Stanford University