CORR-5

Testing versus proving

CorrectnessLesson 5 of 514 min

Tests and proofs do different jobs. A test can show that code is wrong. Only a proof can show that it is right. Good programmers use both, and they choose their tests with a plan.

What tests can and cannot show

A test checks one input. If it fails, you have a counterexample, and the code is wrong. If it passes, you have learned only that the code works for that one input. A function for lists of up to a million values has more possible inputs than any set of tests (a test suite) could ever cover.

That does not make tests weak. Most bugs are found by tests, quickly and cheaply. But a test suite can only find the bugs that its inputs reach, and someone chose those inputs. The rest of this lesson is about choosing them well.

Choosing tests

Good tests come from the spec and from the code:

  • From the spec: the edges of the input condition. Empty, one value, all equal, smallest and largest values allowed.
  • From the code: each branch of every if, a loop that runs zero times, once, and many times.
  • From the proof: the cases where the reasoning was hardest. If the invariant argument needed care when lo == hi, test that case.
  • For speed: the largest input allowed, built so that slow code does the most work.

The practice tests in this course are built in exactly this order, which is why each row has a name.

Stress testing

Often you can write two versions of a function: a slow one that is obviously correct, such as checking every pair, and the fast one you actually want. Then let the computer compare them on thousands of small random inputs. This is called stress testing.

import random

def slow(a):                      # obviously correct: compare every pair
    return any(a[i] == a[j] for i in range(len(a)) for j in range(i + 1, len(a)))

for trial in range(10_000):
    n = random.randint(0, 6)
    a = [random.randint(0, 9) for _ in range(n)]
    if fast(a) != slow(a):
        print("found one:", a)
        break

Small inputs with small values are best. Repeats and edge cases come up often, and a failing input is easy to read. Step through the figure, where a fast that compares only neighbours is run beside a slow that compares every pair.

FIG CORR-5.1Stress testing, then shrinking the failure

fast(a) against slow(a)

Random tests so far
Random listfastslowResult
Rows appear as you step.
phase random tests
1/10

fast(a) says whether a list has a repeated value, but it only compares neighbours. slow(a) compares every pair, so it is surely right. Run both on small random lists and compare the answers.

Step 1 of 10

Making a failing input small

A failing input with 50 values tells you that something is wrong, but not what. So make it smaller. Remove one value. If the test still fails, keep the smaller input. If it now passes, put the value back and try removing a different one. Stop when no single removal keeps the failure. This is called shrinking.

The result, here [1, 7, 1], usually shows the bug at once: two equal values that are not neighbours. Add it to your tests, so that if the bug comes back, a test fails.

Use both

Prove the idea: the invariant, why the loop stops, the cost. Then test the code, because a correct idea can still be typed wrongly. A proof checks the reasoning; tests check the typing. Each catches mistakes the other misses.

From here on, every station gives you both. The lessons prove why each algorithm works. The practice tests try to break your version of it.

CORR-5 counts as completed once you step through the figure to the last step.