Report Number: CS-TR-74-417
Institution: Stanford University, Department of Computer Science
Title: Some thoughts on proving clean termination of programs.
Author: Sites, Richard L.
Date: May 1974
Abstract: Proof of clean termination is a useful sub-goal in the
process of proving that a program is totally correct. Clean
termination means that the program terminates (no infinite
loops) and that it does so normally, without any
execution-time semantic errors (integer overflow, use of
undefined variables, subscript out of range, etc.). In
contrast to proofs of correctness, proof of clean termination
requires no extensive annotation of a program by a human
user, but the proof says nothing about the results calculated
by the program, just that whatever it does, it terminates
cleanly. Two example proofs are given, of previously
published programs: TREESORT3 by Robert Floyd, and SELECT by
Ronald L. Rivest and Robert Floyd.