Summary
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 [3] 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 both correctness and termination by one unified formalism. One can choose to prove total correctness by a single step, or by incremental proof steps, each step establishing more properties of the program.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Floyd, R. W.: Assigning meanings to programs. In: Schwartz, J. T. (ed.): Mathematical aspects of computer science. Proc. Symposia in Applied Mathematics 19. Providence (R.I.): Amer. Math. Soc. 1967, p. 19–32
Hoare, C. A. R.: Algorithm 65-Find. Comm. ACM 4, 321 (1961)
Hoare, C. A. R.: An axiomatic basis of computer programming. Comm. ACM 12, 576–580, 583 (1969)
Hoare, C. A. R.: Proof of a program: FIND. Comm. ACM 14, 39–45 (1971)
Igarashi, S., London, R. L., Luckham, D. C.: Automatic program verification I: A logical basis and its implementation. Computer Science Department, Stanford University, STAN-CS-73-365, May 1973
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Manna, Z., Pnueli, A. Axiomatic approach to total correctness of programs. Acta Informatica 3, 243–263 (1974). https://doi.org/10.1007/BF00288637
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00288637