A property is a statement that holds for every input, such as commutativity or a range bound. Checking properties needs no reference model, only the specification restated as rules.
One property rarely suffices. Four or five independent properties over the full input space catch most single-mistake implementations.
Property kind | Meaning | Adder example |
|---|---|---|
Symmetry | Input order does not matter | add(a, b) equals add(b, a). |
Identity | A neutral input changes nothing | add(a, 0) equals (a, carry 0). |
Wrap rule | Overflow follows modular arithmetic | Sum bits equal (a + b) mod 16. |
Carry rule | The carry flag matches the true sum | Carry is 1 exactly when a + b >= 16. |
Round-trip | Inverse operations cancel | Decoding an encoded value returns the input. |
The program below uses a fake scripted function in place of a model. It checks 4 properties over all 256 operand pairs, then confirms the carry property catches a planted variant with its carry output stuck at 0.
def gen_add4(a, b):
# FAKE stand-in for an assistant-generated 4-bit adder, written for this course
s = a + b
return (s % 16, 1 if s >= 16 else 0)
def plant_add4(a, b):
# FAKE faulty variant with carry output stuck at 0, written for this course
return ((a + b) % 16, 0)
good = 0
for a in range(16):
for b in range(16):
s, c = gen_add4(a, b)
if gen_add4(b, a) == (s, c):
good += 1
if gen_add4(a, 0) == (a, 0):
good += 1
if s == (a + b) % 16:
good += 1
if c == (1 if a + b >= 16 else 0):
good += 1
plant_bad = 0
for a in range(16):
for b in range(16):
if plant_add4(a, b)[1] != (1 if a + b >= 16 else 0):
plant_bad += 1
if good == 1024 and plant_bad == 120:
print("PASS: 256 pairs satisfy 4 properties in 1024 checks, planted variant misses 120 carry checks")
else:
print("FAIL: good=%d plant_bad=%d" % (good, plant_bad))
raise SystemExit(1)256 pairs times 4 properties gives 1024 checks, and all 1024 hold. The planted variant misses exactly 120 carry checks: pairs with a + b >= 16 number 256 - 136 = 120, since sums 0 to 15 take 16 + 15 + ... + 1 = 136 pairs.
The 120 is again the harness proof. A carry rule that never fires on a stuck-at-0 carry is dead code, not a check.
No. It proves these 4 properties hold on these 256 pairs. A mistake outside all four properties still escapes.
Pair (a, b) with sum s has s + 1 solutions while s <= 15. Summing 1 through 16 gives 16 x 17 / 2 = 136.