A large design is proved block by block. Block A is proved under an assumption X about its inputs; block B is proved to guarantee X; then A and B together satisfy A's guarantee, provided the argument has no circle. A black box frees its outputs, so passing proofs stay valid and failures may be spurious. This topic runs each of those statements, including the two ways they go wrong: a circle in which both blocks prove and both are wrong, and a contract that is assumed and never proved.
Lesson | After it you can... |
|---|---|
Run the three proofs, A under X, B guaranteeing X and the top, with a fault in each place. | |
Show a circle that proves a false claim, and repair it by induction on time. | |
Say what a free output keeps and adds, and show the false pass of an unproved contract. | |
Keep a contract table that is checked against the proofs it names. |
Suggested order: top to bottom. The rule first, the circle second because it is the one way the rule fails, black boxes third because they use the rule with an assumed contract, and the table last because it records every contract and its proof.
No: that is a circle. Each proof depends on the other's guarantee and neither has a base case. It needs induction on time, or a proof of one side with no assumption about the other.