Report Number: CS-TR-73-382
Institution: Stanford University, Department of Computer Science
Title: Axiomatic approach to total correctness of programs.
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: July 1973
Abstract: We present here 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). Our extension to Hoare's method lies in the possibility of proving correctness $underline{and}$ termination at once, and in the enlarged scope of properties that can be proved by it.