A formal proof is only as good as its properties and its assumptions: a property that cannot fail proves nothing, and an assumption nobody discharges hides the bug the proof was meant to catch. This section builds both disciplines on the six running designs and on small lesson-local modules, each written for one claim: every claim here has a passing proof and a failing partner that fails for the stated reason at the stated depth. It turns requirement sentences into properties with triggers, windows and scopes; it manages assumptions as a contract with owners and discharging assertions; it scales proofs with data independence, counter and memory abstraction and cut points; it composes block proofs without circles; and it collects the results into reusable property sets.
Topic | What it covers | After it you can... |
|---|---|---|
Five questions per sentence, layering, tracked items, widths and reset | Write a property with a trigger, a window and a failing mutant. | |
Taxonomy, assume versus assert, the review, conversion to assertions | List every assumption with an owner and a discharging assertion. | |
Data independence, counters, memories, cut points | Shrink a proof soundly and name what each abstraction can hide. | |
The rule, the circular trap, black boxes, the contract table | Compose block proofs with no circular dependence. | |
Checker modules, parameters and modes, rule tables per design | Reuse one property set across designs, sizes and modes. |
Suggested order: top to bottom. Properties first, because everything else assumes they can fail; assumptions second, because every proof is relative to them; abstraction third, because scale comes after correctness; composition fourth, because contracts close the loops the earlier topics open; reuse last, because a library collects what the section proved.
Writing properties first: whether the trigger can ever fire, and whether the property compares against an independent expectation. Assumptions second: what the proof assumed away.