Dry runs and loop invariants

“Walk me through your code with this input” is a request to expect in a live round. Sometimes the editor cannot run code at all; sometimes the interviewer simply wants to see whether you can find a bug without a computer. A dry run done as a table, plus one sentence that says what the loop keeps true, turns that from guesswork into a check. This lesson shows both on a partition loop, catches a loop that stops one step early, and then uses the same idea to settle the boundaries of a binary search, where off-by-one errors are most at home.

A dry run is a table

Pick a small input that reaches every branch of the code, five values or so. Then draw a table with one column for each variable that changes and one row for each pass of the loop, and fill it in as the code would, line by line. Five to eight rows are enough; more means the input is too big.

Here is the code, a partition that moves every value below a pivot to the front of the list, and the table it prints when it runs on [3, 8, 1, 8, 2] with the pivot 4:

def partition(values, pivot, trace=print):
    """Move every value below pivot to the front, in place; return how many there are."""
    write = 0
    trace(f"{'read':>4}  {'value':>5}  {'action':<13}{'write':>5}  values")
    trace(f"{'-':>4}  {'-':>5}  {'start':<13}{write:>5}  {values}")
    for read in range(len(values)):
        # Invariant: values[:write] are all below pivot, values[write:read] are all at least pivot.
        value = values[read]
        if value < pivot:
            values[write], values[read] = values[read], values[write]
            action = f"swap into {write}"
            write += 1
        else:
            action = "leave"
        assert all(v < pivot for v in values[:write])  # the invariant, checked after every pass
        assert all(v >= pivot for v in values[write : read + 1])
        trace(f"{read:>4}  {value:>5}  {action:<13}{write:>5}  {values}")
    return write


if __name__ == "__main__":
    values = [3, 8, 1, 8, 2]
    count = partition(values, 4)
    print(f"{count} values below 4 are at the front: {values[:count]}")

read  value  action       write  values
   -      -  start            0  [3, 8, 1, 8, 2]
   0      3  swap into 0      1  [3, 8, 1, 8, 2]
   1      8  leave            1  [3, 8, 1, 8, 2]
   2      1  swap into 1      2  [3, 1, 8, 8, 2]
   3      8  leave            2  [3, 1, 8, 8, 2]
   4      2  swap into 2      3  [3, 1, 2, 8, 8]
3 values below 4 are at the front: [3, 1, 2]

Two pointers walk the list. read looks at each value once; write marks where the next value below the pivot goes. When read finds such a value, it is swapped into position write, and write moves on. In an interview you fill in exactly this table by hand, saying each row aloud: “read is 2, the value is 1, below the pivot, so it swaps into position 1 and write becomes 2.”

The invariant behind the table

The two assert lines inside the loop check one sentence after every row, the loop’s invariant: everything before write is below the pivot, and everything from write up to read is at least the pivot.

An invariant is useful because three short arguments together prove that the loop works:

1. Initialisation: it is true before the first pass. write and read both start at 0, so both parts are empty, and a statement about every value of an empty part is true.
2. Maintenance: each pass keeps it true. A value below the pivot is swapped to the end of the first part, and both parts move on together; any other value simply joins the second part.
3. Termination: the loop ends, and then the invariant gives the answer. read grows by one every pass, so the loop stops after len(values) passes. Then nothing is left unlooked at, so the invariant says that every value below the pivot is at the front, and write is how many of them there are.

C. A. R. Hoare’s paper on an axiomatic basis for computer programming, which builds on earlier work by Robert Floyd, turned this way of reasoning into a rule: its rule for a while loop is built around exactly such a statement. The DSA track’s lesson on correctness treats it more formally. For a coding round, the practical habit is short: write the invariant as a comment at the top of the loop, as partition.py does, and check it against each row of your dry run.

assert costs nothing to try while you practise, but do not rely on it in code you hand in: Python skips assert statements entirely when it runs with the -O option.

A common mistake: stopping one step early

Here is the same partition with a loop bound that looks reasonable and is one short:

def partition_early(values, pivot):
    """The same partition, but the loop stops one step early."""
    write = 0
    for read in range(len(values) - 1):  # the last value is never looked at
        if values[read] < pivot:
            values[write], values[read] = values[read], values[write]
            write += 1
        print(f"read {read}: write {write}, {values}")
    # On exit the part still to look at, values[read + 1:], should be empty.
    assert read + 1 == len(values), f"values[{read + 1}:] = {values[read + 1:]} was never looked at"
    return write


partition_early([3, 8, 1, 8, 2], 4)

read 0: write 1, [3, 8, 1, 8, 2]
read 1: write 1, [3, 8, 1, 8, 2]
read 2: write 2, [3, 1, 8, 8, 2]
read 3: write 2, [3, 1, 8, 8, 2]

Traceback (most recent call last):
  File "stops_early.py", line 14, in <module>
    partition_early([3, 8, 1, 8, 2], 4)
    ~~~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^
  File "stops_early.py", line 10, in partition_early
    assert read + 1 == len(values), f"values[{read + 1}:] = {values[read + 1:]} was never looked at"
           ^^^^^^^^^^^^^^^^^^^^^^^
AssertionError: values[4:] = [2] was never looked at

Every row of the trace still keeps the invariant, which is the point: the mistake is not in what the loop does but in where it stops. The final assert checks the termination step, that nothing is left unlooked at, and fails on the last value, 2, which never reached the first part. A dry run catches it the same way: when you write the last row, ask what is left after it. Many off-by-one errors are questions about the first or the last row that nobody asked.

Boundaries come from the invariant

Binary search is where boundaries cause the most trouble: < or <=, mid or mid + 1, hi = len(a) or len(a) - 1. Choose them from an invariant instead of from memory. To find the first position whose value is at least x in a sorted list, keep this invariant:

Each boundary then follows from it:

• Start with lo = 0 and hi = len(a). Nothing is known yet, and the answer may be len(a), when every value is below x.
• Loop while lo < hi. The part not yet known is a[lo:hi]; the loop runs while it is not empty.
• mid = (lo + hi) // 2 is always at least lo and below hi, so it lies inside the unknown part.
• If a[mid] < x, set lo = mid + 1. a[mid] is now known to be below x, so it joins the part before lo. Setting lo = mid would leave it unknown, and when hi is lo + 1 the loop would never move again.
• Otherwise set hi = mid. a[mid] is at least x and might be the answer, so it becomes the first value of the part from hi on. hi = mid - 1 would throw it away.
• The loop ends because hi - lo gets smaller on every pass. When lo == hi, nothing is unknown, and lo is the answer.

Here is that search, with its trace table, checked against Python’s own bisect.bisect_left:

import bisect
import random


def lower_bound(a, x, trace=None):
    """The first position in the sorted list a whose value is at least x (len(a) if none is)."""
    lo, hi = 0, len(a)
    # Invariant: every value before lo is below x, every value from hi on is at least x.
    while lo < hi:  # the part not yet known, a[lo:hi], is not empty
        mid = (lo + hi) // 2  # lo <= mid < hi, so mid is always inside the unknown part
        if a[mid] < x:
            decision = "below x: lo = mid + 1"
            lo = mid + 1  # a[mid] is known to be below x, so it leaves the unknown part
        else:
            decision = "at least x: hi = mid"
            hi = mid  # a[mid] might be the answer, so it stays at the edge of the unknown part
        if trace:
            trace(mid, a[mid], decision, lo, hi)
    return lo  # lo == hi: nothing is unknown, and values from lo on are at least x


if __name__ == "__main__":
    a = [1, 3, 3, 6, 6, 9]
    print(f"Searching {a} for the first value at least 6")
    print(f"{'mid':>3}  {'a[mid]':>6}  {'decision':<24}{'lo':>3}{'hi':>4}")

    def show(mid, value, decision, lo, hi):
        print(f"{mid:>3}  {value:>6}  {decision:<24}{lo:>3}{hi:>4}")

    answer = lower_bound(a, 6, trace=show)
    print("Answer:", answer)

    rng = random.Random(9)
    for _ in range(2_000):
        a = sorted(rng.randint(0, 9) for _ in range(rng.randint(0, 8)))
        x = rng.randint(-1, 10)
        assert lower_bound(a, x) == bisect.bisect_left(a, x), (a, x)
    print("2,000 random lists: lower_bound agrees with bisect.bisect_left")

Searching [1, 3, 3, 6, 6, 9] for the first value at least 6
mid  a[mid]  decision                 lo  hi
  3       6  at least x: hi = mid      0   3
  1       3  below x: lo = mid + 1     2   3
  2       3  below x: lo = mid + 1     3   3
Answer: 3
2,000 random lists: lower_bound agrees with bisect.bisect_left

The trace shows the invariant at work: each row moves either lo or hi and never past the other. The Python documentation describes bisect_left’s result in the same terms: everything before the returned position is less than x, and everything from it on is at least x. That is this loop’s invariant at the moment it stops, which is why the 2,000 random comparisons agree.

Dry-running in a round

• Choose the input on purpose. Small, but reaching every branch, and ending with the edge case you are least sure of: an empty list, a single value, or a value at the boundary.
• Write the invariant first, as a comment above the loop, in one sentence. If you cannot write it, you are not yet sure what the loop does.
• Trace the first and the last rows slowly. The middle rows are usually fine; the boundaries are where loops fail.
• Say the values aloud. It keeps the interviewer with you, and saying “so i is now 3, which is past the end” is often how you notice the bug.

Try it on this five-line program before looking at what it printed:

values = [5, 1, 4]
total = 0
for i in range(len(values) - 1):
    total += values[i]
print(total)

6

The loop adds values[0] and values[1] and stops: range(len(values) - 1) is one short again. If the comment above the loop said “total is the sum of values[:i + 1]”, the last row of your table, i = 1, would have shown at once that the last value is missing.

Key takeaways

• A dry run is a table: one column per changing variable, one row per pass, five to eight rows on a small input that reaches every branch.
• An invariant is a sentence the loop keeps true. Check that it holds at the start, that each pass keeps it, and that when the loop ends it gives the answer.
• Off-by-one errors are usually about the first or the last row: trace those slowly, and ask what is left after the loop stops.
• Choose boundaries from the invariant: while lo < hi, lo = mid + 1 when a[mid] is known to be too small, hi = mid when it might be the answer.