Chapter Four
Proving Programs Terminate Using Well-Founded Orderings, Ramsey's Theorem, and Matrices
William Gasarch Department of Computer Science, University of Maryland, College Park, Maryland, USA
Abstract
Many programs allow the user to input data several times during its execution. If the program runs forever, the user may input data infinitely often. A program terminates no matter what the user does. We define a program to terminate if no matter what the user does the program will halt.
We discuss various ways to prove that a program terminates. The proofs use well-founded orders, Ramsey Theorem, and matrices. These techniques are used by real program checkers.
General Terms
Verification
Theory
Keywords
Proving programs terminate ...
