A passing test is not a proof
A test runs a program on a few inputs and checks the answers. A test can show that a bug exists, but it can never show that no bug exists.
A formal method asks a tool to check every input at once. Here you meet both on one small price function from a shop.
By the end of this lesson
Note
I can say what a test shows and what a proof shows.
Key words
| Word | What it means |
|---|---|
| Test case | one input with the answer you expect |
| Bug | a mistake in a program |
| Specification | a written statement of what a program must do |
| Proof | a check that covers every possible case |
| Counterexample | one case that breaks a claim |
| Formal method | a way to check a design with a tool |
The cells students fill in are left blank in this preview.
A test only checks the cases you chose
A shop charges 250 pence for each item. From 20 items on, each item costs 225 pence, a 10% discount.
A developer writes n > 20 where the rule says "from 20". The shop team tests 5, 10 and 30 items. All three pass, and the bug stays hidden.
Three tests pass, one case is wrong
def right_total(n):
# From 20 items, each item costs 225 pence.
if n >= 20:
return n * 225
return n * 250
def shop_total(n):
# The bug: > instead of >=.
if n > 20:
return n * 225
return n * 250
tested = [5, 10, 30]
for n in tested:
print(n, shop_total(n) == right_total(n))
wrong = []
for n in range(1, 101):
if shop_total(n) != right_total(n):
wrong.append(n)
print("wrong for:", wrong)
# Add 20 to the tested list and run again.
A proof covers every case at once
The loop above tried 100 cases because we could afford to. A real price can be any whole number, so a loop can never try them all.
A solver such as Z3 does not loop. It reasons about a number n that stands for every whole number. The next two Runs ask Z3 about the shop function. Z3 reads rules in a bracketed form, shown in the table.
Worked example: Python written for Z3
| In Python | In Z3 | What it says |
|---|---|---|
| n >= 20 | (>= n 20) | n is at least 20 |
| n * 225 | (* n 225) | n times 225 |
| a if n >= 20 else b | (ite (>= n 20) a b) | a when n is at least 20, otherwise b |
| x != y | (not (= x y)) | x is not equal to y |
The cells students fill in are left blank in this preview.
Search a million item counts
echo '(declare-const n Int) (assert (and (>= n 1) (<= n 1000000))) (assert (not (= (ite (> n 20) (* n 225) (* n 250)) (ite (>= n 20) (* n 225) (* n 250))))) (check-sat) (get-model)' | z3 -inShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Prove a total is never negative
echo '(declare-const n Int) (assert (>= n 1)) (assert (< (ite (>= n 20) (* n 225) (* n 250)) 0)) (check-sat)' | z3 -inShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
A common mistake
Warning
Many people think a proof means the program has no bugs. A proof covers only the claim you wrote. "The total is never negative" is true even of the buggy shop function, because the claim says nothing about the discount. Prove the rule you actually care about.
What tests and proofs each show
| Question | A test | A proof |
|---|---|---|
| Cases covered | The ones you pick | Every case the claim names |
| Can it find a bug? | Yes, if you pick the case | Yes, and it names the case |
| Can it show there is no bug? | Never | Yes, for the claim you wrote |
| What it needs | The program | The program and a written claim |
The cells students fill in are left blank in this preview.