Insertion sort & the loop-invariant method

The incremental method

Insertion sort builds the answer one element at a time, exactly like sorting a hand of playing cards: keep the cards already in your hand sorted, pick up the next card, and slide it leftward past every larger card until it sits in its place. The already-sorted region grows by one each round until the whole hand is sorted.

CLRS writes the array 1-indexed. The outer loop runs $i$ from $2$ to $n$; key = A[i] is the card being inserted, and the inner while shifts each larger neighbour one slot right to open a gap for it:

INSERTION-SORT(A, n)
  for i = 2 to n
    key = A[i]
    j = i - 1
    while j > 0 and A[j] > key
      A[j + 1] = A[j]
      j = j - 1
    A[j + 1] = key

The loop invariant: proving it correct

A loop invariant is a property true *before every iteration* of a loop. Proving it is the algorithmic analogue of induction, and it is a near-guaranteed exam task. For insertion sort the invariant is:

> At the start of each iteration of the for loop, the subarray $A[1..i-1]$ consists of the elements originally in $A[1..i-1]$, but in sorted order.

Notice the two clauses: *same elements* (nothing lost or invented) and *sorted*. Stating only "the left part is sorted" throws away the elements clause and the proof collapses. You discharge an invariant in three steps:

1. Initialization (the base case). Before the first iteration $i = 2$, so $A[1..i-1] = A[1..1]$ is a single element — trivially sorted and trivially the original element. ✓
2. Maintenance (the inductive step). Assume the invariant before iteration $i$. The body moves $A[i-1], A[i-2], \dots$ one position right until it finds the slot where key belongs, then drops key in. So $A[1..i]$ now holds the same elements, in sorted order — the invariant holds before iteration $i+1$. ✓
3. Termination (the payoff). The loop ends when $i = n+1$. Substituting $i = n+1$ into the invariant gives: $A[1..n]$ holds the original elements in sorted order — exactly the sorting postcondition. ✓

The three steps map onto base case / inductive step / conclusion. The conclusion step is the one that matters most: it is where you *extract* correctness by plugging the loop variable's final value into the invariant.

Properties

Insertion sort is in-place ($\Theta(1)$ extra memory) and stable (equal keys keep their relative order, because the strict A[j] > key test never moves an equal element). Its running time depends on the input, not just its size:

- Best case — input already sorted. The while test fails immediately every round, so total work is $\Theta(n)$. - Worst case — input reverse-sorted. Element $A[i]$ shifts past all $i-1$ predecessors, so the total shift count is $\sum_{i=2}^{n}(i-1) = \frac{n(n-1)}{2} = \Theta(n^2)$. - Average case — each element lands about halfway into the sorted prefix, $\approx n^2/4$ shifts: still $\Theta(n^2)$.

That $\Theta(n)$ best case is why production sorts (Timsort) fall back to insertion sort on small or nearly-sorted runs.