A Full Proof: Insertion Sort and Binary Search

Assembling the toolkit

This rung has handed you four separate tools, and so far you have met each one on its own. From why tests are not proofs you learned that running an algorithm on a few inputs only ever shows what it did, never what it must do. From the loop invariant you got a statement that stays true across every turn of a loop, checked by initialization, maintenance, and a termination read-off. From induction you got the engine that powers that maintenance step. And from the decreasing measure you got a way to prove the loop actually stops. Now we use all four at once on real code.

The shape of every full proof in this guide is the same, and it is worth holding in your head before the details arrive. First we pin down a precondition (what we assume on the way in) and a postcondition (what we promise on the way out). Then a loop invariant carries us across the loop, and reading it at loop exit hands us the postcondition — that is partial correctness, the promise if the algorithm halts. Then a separate decreasing measure proves it does halt. Partial correctness plus termination equals total correctness: it stops, and when it stops, the answer is right.

Insertion sort: setting up the contract

Insertion sort grows a sorted region one element at a time, the way you tidy a hand of playing cards: you keep the cards already in your hand sorted, pick up the next card, and slide it leftward past every card bigger than it until it lands in its place. Here is the pseudocode we will prove correct, indexing the array A from 1 to n.

INSERTION-SORT(A, n):
  for j = 2 to n:               # outer loop
      key = A[j]
      i = j - 1
      while i >= 1 and A[i] > key:   # inner loop
          A[i+1] = A[i]
          i = i - 1
      A[i+1] = key

Now the contract. The precondition is mild: A is an array of n comparable items (any order). The postcondition is what "sorted" really means, and we must say it precisely or we cannot prove it: at the end, A[1] <= A[2] <= ... <= A[n], and the final array is a permutation of the original. That second half matters and is easy to forget — an algorithm that overwrote everything with zeros would produce a perfectly non-decreasing array while destroying the data. A real sort must rearrange, not invent.

Insertion sort: the invariant proof and why it halts

The whole proof hangs on one well-chosen loop invariant for the outer for-loop. Here it is, in words first: at the start of each iteration with index j, the subarray A[1..j-1] holds the same elements that originally sat in A[1..j-1], now in sorted order. This is exactly the insertion sort invariant. Notice it bundles in both halves of the postcondition — sorted and a permutation of what was there — so that when the loop ends, both promises fall out together.

1. Initialization. Before the first iteration j = 2, the region A[1..j-1] is just A[1..1], a single element. One element is trivially sorted and is trivially the same one element that started there. The invariant holds before the loop even begins — the base case is free.
2. Maintenance. Assume the invariant holds at the start of iteration j: A[1..j-1] is a sorted permutation of the originals. The inner while-loop slides key = A[j] leftward, copying each larger element one slot right, and stops the moment it meets an element <= key (or runs off the left edge). Dropping key into that gap inserts it at exactly the right rank, so A[1..j] is now sorted; and since we only moved elements and re-placed key, A[1..j] is still a permutation of the original A[1..j]. That is precisely the invariant for the next iteration j+1.
3. Termination read-off. The for-loop stops when j has just passed n, i.e. when the region A[1..j-1] is the whole array A[1..n]. Plug that into the invariant: A[1..n] is a sorted permutation of the original A[1..n]. That is word-for-word the postcondition. Partial correctness, done.

One honest gap remains in that maintenance step: it quietly assumed the inner while-loop does what we said and then halts. The inner loop owes its own sub-proof, and it has its own tiny invariant — "the elements shifted right so far are all > key" — plus its own decreasing measure: the index i strictly drops by 1 each pass and is bounded below by 0, so it cannot run forever. Real proofs nest like this, a loop inside a loop each carrying its own invariant; skipping the inner one is the single most common way a sorting proof secretly cheats.

The invariant gave us partial correctness — if insertion sort halts, the output is sorted. To upgrade to total correctness we still owe outer-loop termination, and the decreasing-measure argument settles it cleanly. Take the measure to be the number of iterations still to run, n - j + 1. Each pass of the for-loop increases j by exactly one, so this measure strictly decreases each time and is bounded below by zero — a non-negative integer that strictly drops every step cannot do so forever, so the outer loop must terminate. Combined with the inner loop's own measure (the index i shrinking toward 0), every loop is guaranteed to stop. Stitch the pieces: partial correctness from the invariant, plus termination from the two decreasing measures, gives total correctness. Insertion sort always halts, and whenever it halts the array is sorted — proven, not merely observed on the test cases we happened to try.

Binary search: the same recipe, a sharper invariant

Binary search hunts for a target x in a sorted array A[1..n] by repeatedly halving a window [lo, hi]. Its precondition is the load-bearing one — A must be sorted, and the proof leans on that hard. The postcondition: return an index i with A[i] = x if x is present, else report "absent." The same four-tool recipe applies, but the invariant now captures a search-space claim rather than a sorted-prefix one.

Here is the binary search invariant: if x is anywhere in A at all, then it lies within the current window A[lo..hi]. Initialization is immediate — we start with lo = 1, hi = n, so the window is the whole array and the claim is trivially true. Maintenance is where the sortedness earns its keep: compare x with the midpoint A[mid]. If x < A[mid], then because A is sorted every element from mid rightward is also > x, so x (if present) cannot be there — we safely set hi = mid - 1 and the invariant survives. The symmetric case sets lo = mid + 1. We never throw away the half that could contain x.

Binary search: reading off the answer, and why it halts

The termination read-off is subtler than insertion sort's, because binary search can leave in two ways. If at some midpoint A[mid] = x, we return mid — done, and the answer is correct because we literally checked A[mid] = x. Otherwise the loop ends when the window empties, lo > hi. Now invoke the invariant: it promised that if x were in A it would be inside [lo..hi]. But [lo..hi] is now empty, so x cannot be in A — we correctly report "absent." The invariant did the heavy lifting: an empty window plus the invariant is a proof of absence, not a guess.

Termination uses the decreasing measure once more, and here the measure is the window's size, hi - lo + 1. Every iteration either returns (and we are done) or strictly shrinks the window by discarding a non-empty half, so the size drops by at least one and is bounded below by zero. It therefore cannot shrink forever; the loop must stop. A subtle pitfall lives exactly here: a careless off-by-one — say setting hi = mid instead of hi = mid - 1 — can leave the window the same size on some step, the measure fails to strictly decrease, and you get an infinite loop. The decreasing-measure proof is what forces you to get those updates exactly right.

Step back and admire the symmetry. Two very different algorithms, one rearranging data and one searching it, both yielded to the identical four-move recipe: state the precondition and postcondition, choose an invariant that bundles the postcondition inside it, prove initialization-maintenance-termination, then close the deal with a decreasing measure. This is the same skeleton behind the Euclid GCD proof and behind correctness arguments for far more elaborate algorithms you will meet higher up the ladder. The technique scales; only the choice of invariant gets cleverer.

What a proof buys, and what it does not

Be honest about the scope of what we just established. We proved these two algorithms correct — that they compute the right answer and halt. That is a statement about the algorithm on the idealized machine model, and it is silent about cost. Insertion sort is provably correct yet runs in Theta(n^2) in the worst case; binary search is provably correct in O(log n). Correctness and efficiency are different questions answered by different machinery — an invariant tells you whether the answer is right, never how fast you reached it.

Two more boundaries worth naming. First, a proof is only as good as its model: we assumed integer comparisons take a fixed step and that array reads are exact. Real machines have overflow, floating-point rounding, and finite memory; the famous binary-search overflow bug (mid = (lo + hi) / 2 overflowing on huge arrays) was a flaw not in the math but in the assumed arithmetic. A correctness proof certifies the algorithm, and a faithful implementation is a separate obligation. Second, our proof certifies this algorithm meets this spec — it says nothing about whether the spec itself is the one you wanted. Garbage postcondition in, garbage guarantee out.

None of these caveats weaken the method; they sharpen how you wield it. A loop invariant plus a decreasing measure is the most reliable way humans know to be certain a piece of code does what it claims, across all of the infinitely many inputs that testing can never reach. With this rung complete, you can read an unfamiliar algorithm and ask the right questions — what is the invariant, what is the measure, where is the precondition consumed — and that habit is precisely what separates believing an algorithm works from knowing it.