Loop Termination (Hoare Calculus)

hoare-calculus program-proofing

Definition

Loop Termination

Loop termination is the proof obligation that a while loop eventually stops for all inputs satisfying the given precondition.

In Hoare calculus, termination is usually shown with a loop variant (also called a termination function): a mapping from the program state to a well-founded set, typically the natural numbers $\mathbb{N}$, that strictly decreases with each iteration.

Idea

A termination proof has two parts:

• a loop invariant to show partial correctness;
• a loop variant to show that the loop cannot continue forever.

The invariant says what stays true during the loop. The variant measures progress. Since the variant is well-founded and decreases strictly, the loop can only execute finitely many times.

Verification

For a loop while e do Π od, one typically shows:

1. there is a variant $t$ with an initial value $t_0$;
2. $t$ is bounded below, usually by $0$;
3. every loop iteration makes $t$ strictly smaller;
4. the invariant still holds.

A common form is:

$$\frac{\{Inv\wedge e\wedge t=t_0\}\Pi \{Inv\wedge 0\le t<t_0\}}{\{Inv\}\mathbf{while}e\mathbf{do}\Pi \mathbf{od}\{Inv\wedge \neg e\}}$$

This means that the body preserves the invariant and decreases the variant.

Alternative Formulations

Sometimes the termination obligation is written by separating the partial-correctness part from the variant condition:

$$\{Inv\wedge e\}\Pi \{Inv\}$$

and additionally showing that the variant decreases:

$$Inv\wedge e\wedge t=t_0⟹0\le t<t_0$$

The second condition is what guarantees termination.

Example

Decreasing counter

Consider the following annotated loop:

{x ≥ 1}
while x > 1 do
    x := x - 1
od
{x = 1}

The loop variant is $t=x$.

• It is bounded below by the precondition $x\ge 1$.
• It decreases by $1$ in every iteration.
• It cannot decrease forever.

Therefore, the loop terminates.

precondition or the loop invariant. In this example, the precondition $x\ge 1$ guarantees that the variant $t=x$ never drops below $1$ while the loop runs. Since it strictly decreases, it can only do so finitely many times.

The lower bound is not automatic. It must be derived from the

Total Correctness totally correct only if it is partially correct and its loops terminate.

A program is