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 ...

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.