BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-73-382
       ENTRY:: September 25, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Axiomatic approach to total correctness of programs.
        TYPE:: Technical Report
      AUTHOR:: Manna, Zohar
      AUTHOR:: Pnueli, Amir
        DATE:: July 1973
       PAGES:: 27
    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.
       NOTES:: [Adminitrivia V1/Prg/19950925]
         END:: STAN//CS-TR-73-382