= Algorithm termination
<Algorithm termination> means that execution finishes after finitely many steps on the <inputs> under consideration. Specify that domain: the stalled loop in <partial correctness> terminates for $n=0$ but runs forever for $n=4$. A successful run on one <input> does not establish termination on another.
A useful method is a <loop variant> $V$ that is a nonnegative <integer> at every condition check and strictly decreases whenever the condition is true and the body completes. Also prove that condition evaluation and each body execution terminate. An infinite run would then give an infinite strictly decreasing <sequence> of nonnegative <integers>, contradicting their <well-founded relation>. This establishes <algorithm termination> without enumerating all executions.
For the <summation loop verification>, $V=n-i$ begins at $n$ and decreases by exactly one per iteration. The body executes exactly $n$ times, including zero times for $n=0$. Merely bounding a decreasing measure below is insufficient for <real numbers>: $1,1/2,1/4,\ldots$ decreases forever while staying positive. The choice of a <well-founded relation> supplies the essential progress argument; <well-founded progress in recursion> applies the same idea to <recursive calls>.
Back to article page
