Loop Invariants and Correctness

The Three-Part Correctness Framework

An algorithm is correct if, for every input instance, it terminates with the correct output. For algorithms containing loops, we prove correctness using a loop invariant: a logical statement that remains true at the start of every loop iteration.

The proof has three parts:

1. Initialisation: The invariant is true before the first iteration.
2. Maintenance: If the invariant is true at the start of an iteration, it remains true at the end (and thus at the start of the next iteration).
3. Termination: When the loop exits, the invariant combined with the exit condition proves the postcondition (the algorithm’s goal).

Partial vs Total Correctness

Partial correctness: if the algorithm terminates, it produces the correct answer. Total correctness: partial correctness plus a guarantee that the algorithm always terminates. For Insertion Sort, the FOR loop counts upward from 2 to $n$ (finite), and each inner WHILE loop counts downward from a positive value (well-founded), so it is totally correct.

Proving Insertion Sort Correct

The algorithm:

1. for j = 2 to A.length
2.  Key = A[j]; i = j - 1
3.  while i > 0 and A[i] > Key
4.   A[i+1] = A[i]; i = i - 1
5.  A[i+1] = Key

Invariant

P: At the start of each iteration of the FOR loop, the subarray $A[1 \dots j-1]$ contains the elements originally in positions $1 \dots j-1$, in sorted order.

Initialisation ($j = 2$)

$A[1 \dots 1]$ is a single-element subarray, trivially sorted. ✅

Maintenance

Assume $A[1 \dots j-1]$ is sorted at the start of the iteration. The WHILE loop shifts elements greater than Key one position right, creating a gap at the correct insertion point. When the loop exits, A[i+1] receives Key, and $A[1 \dots j]$ is now sorted. The invariant holds for the next iteration. ✅

Termination ($j = n+1$)

When the FOR loop ends, $j = n+1$. Substituting into the invariant, $A[1 \dots n]$ (the whole array) is sorted, which is exactly the postcondition. ✅

Example Walkthrough

Input: $[9, 102, 10, -7]$

j	Key	Before WHILE	After WHILE	Sorted prefix
2	102	$[9, 102, 10, -7]$	$[9, 102, 10, -7]$	$[9, 102]$
3	10	$[9, 102, 10, -7]$	$[9, 10, 102, -7]$	$[9, 10, 102]$
4	-7	$[9, 10, 102, -7]$	$[-7, 9, 10, 102]$	sorted

Choosing a Useful Invariant

Not every true statement is a useful invariant. The statement $1 = 1$ satisfies initialisation and maintenance but proves nothing about sorting at termination. The invariant must relate program variables to the desired postcondition. It must be strong enough to imply the result upon termination but weak enough to be provably maintained.

Summary

Step	What to check
Initialisation	Invariant holds before first iteration
Maintenance	If invariant holds before, it holds after one iteration
Termination	Invariant + exit condition $\Rightarrow$ postcondition
Partial correctness	Correct if it terminates
Total correctness	Correct plus guaranteed termination
Key invariant	$A[1 \dots j-1]$ is sorted (Insertion Sort)