REFERENCE SHEET

Recursion, invariants & termination

A correct output and a guaranteed halt are separate obligations.

{P} C {Q}: if C starts in P and terminates, its final state satisfies Q

Definitions

Loop invariant

A statement that holds before the loop and is preserved by every iteration. Combined with the exit condition, it should imply the desired postcondition.

Partial vs total correctness

Partial correctness asserts the postcondition whenever the program terminates. Total correctness additionally asserts termination on every permitted input.

Recursive specification

A problem expressed through smaller instances, with base cases. A well-founded measure must decrease along recursive calls to justify termination.

Key theorems

Invariant proof rule

Establish initialization, preservation, and that invariant plus loop exit implies the postcondition. These prove partial correctness.

Termination by a variant

If a nonnegative integer measure strictly decreases on every iteration while the loop continues, the loop terminates.

Euclidean algorithm

For nonnegative integers a,b, not both zero, repeated replacement (a,b)←(b,a mod b) while b≠0 terminates with a=gcd(a₀,b₀). The gcd is invariant and the second component strictly decreases.

Notable applications

Search routines

A binary-search invariant specifies exactly which interval can still contain the answer.

Verification

State preconditions explicitly to catch overflow, invalid indices, and missing base cases.

Work it out

Try before revealing

01 / Trace

Run Euclid on (48,18).

Hint

At each step compute the remainder.

Solution

(48,18)→(18,12)→(12,6)→(6,0). The gcd is 6.

02 / Prove

For n≥0, a loop starts i=0,s=0 and repeatedly sets s←s+i+1, i←i+1 until i=n. Give an invariant and termination measure.

Hint

Relate s to the numbers processed so far.