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
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.
Proving programs terminate ...
Get Advances in Computers now with O’Reilly online learning.
O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.