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[\mathrm{1..}i-1]$ consists of the elements originally in $A[\mathrm{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[\mathrm{1..}i-1]=A[\mathrm{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[\mathrm{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[\mathrm{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.