Termination proof
From Wikipedia, the free encyclopedia
A termination proof is a type of mathematical proof that plays a critical role in formal verification because total correctness of an algorithm depends on termination.
A simple, general method for constructing termination proofs involves associating a measure with each step of an algorithm. The measure is taken from the domain of a well-founded relation, such as from the ordinal numbers. If the measure "decreases" according to the relation along every possible step of the algorithm, it must terminate, because there are no infinite descending chains in a well-founded set.
Some types of termination analysis can automatically generate or imply the existence of a termination proof.
