The Altrincham projectA loop invariant for binary search
One sentence that stays true on every pass, and what happens when it does not.
Ordnance Survey's open postcode file lists 2,316 postcodes in the WA14 and WA15 districts, already in sorted order. Most are in Trafford; the file also places 75 of them in Cheshire East and 17 in Manchester, so this is a list of two postcode districts and not a list of Altrincham alone. The learner writes a binary search over it. Two markers, lo and hi, fence off the part of the list still in play. The invariant is this: if the postcode we want is in the list at all, it is somewhere from position lo up to, but not including, position hi. It must be true before the loop starts and after every pass. In Python that is one assert line inside the loop.
The correct search finds all 2,316 postcodes. It never needs more than 12 looks at the list and averages 10.24, where reading from the top could need 2,316. It also correctly reports 2,000 made-up postcodes as absent. Then the learner is handed three other versions. Each differs from the correct one by a single character or number, the kind of slip that people and AI assistants both make.
Four versions of binary search on 2,316 WA14 and WA15 postcodes, plus 2,000 made-up postcodes not in the list (our Python run on OS Code-Point Open)| Version | Real postcodes not found | Made-up postcodes that never finish | What catches it |
|---|
| Correct | 0 | 0 | Nothing to catch |
| A: hi starts one place too low | 1 | 0 | Reading the first line against the invariant |
| B: lo = mid in place of mid + 1 | 0 | 1,998 | A check that the window shrinks |
| C: hi = mid - 1 in place of mid | 1,023 | 0 | The assert, on the pass that loses the target |
Version C is the loud one. It fails on 1,023 postcodes, 44.2% of the list, so almost any testing would notice, and the assert points at the exact pass where the target was thrown away. Version A is the quiet one. It works for 2,315 postcodes and fails on one: WA15 9YS, the very last in the list, which never gets inside the window. If you tested it on 20 postcodes picked at random, it would pass all 20 about 99.1% of the time. An assert inside the loop is no luckier: at run time it trips on WA15 9YS and on nothing else, one search in 2,316. What exposes version A is reading the first line against the invariant. With hi starting one place too low, the promise "if the target is in the list, it is between lo and hi" is already broken for the last postcode before the loop begins. No test input is needed to see that, and the invariant names the one test worth writing: search for the last item.
Version B teaches a second rule. It finds every real postcode, and its invariant is never broken. But give it a postcode that is not in the list and the window stops shrinking: 1,998 of our 2,000 made-up postcodes never finished, and we stopped each after 200 looks. A test suite that only searches for things that exist would pass it completely. So a proof of a loop needs two parts: an invariant, which shows the answer is right if the loop ends, and a quantity that gets smaller on every pass, which shows the loop does end. Here that quantity is hi minus lo.
Ages 8 to 11
Play guess-the-number with a rule card: "the secret is always between my two fingers". Spot when it breaks.
Ages 11 to 15
Write binary search in Python, add the assert, and search for every postcode in the list.
Ages 15 and up
Diagnose versions A, B and C, state the invariant and the shrinking quantity, and test absent items too.
Data note
Contains OS data (C) Crown copyright and database right 2026 (Code-Point Open, Open Government Licence), read 30 September 2026. The four search versions, the made-up postcodes and all counts are our own work. Only the postcode strings are used; nothing about any address or resident is involved.
