Proof and Model Contracts

A theorem and a passing program answer different questions. Attach this short contract to each proof, lab and capstone artifact.

Obligation	What to record	Example failure
Universe	Every variable's domain; whether empty inputs are allowed	Treating an integer witness as a real witness without checking the claim
Claim	Exact hypotheses, conclusion and quantifier order	Replacing one witness per input with a common witness
Definitions	Total/partial function; relation direction; tree grammar	Calling a multivalued relation a function
Proof	General argument or complete finite enumeration with coverage	Presenting 100 successful integer tests as a universal proof
Representation	What code values denote and how equality works	Counting shared objects instead of tree occurrences
Execution	Arithmetic, termination and finite resource assumptions	Treating a decreasing positive real as a termination measure

Conventions used here

We use classical logic and N={0,1,2,...}. An implication is false only when its hypothesis is true and its conclusion false. Empty universal quantification is true; empty existential quantification is false. A mathematical predicate must have a truth value on its whole declared domain.

A typed function includes its domain, codomain and graph. Equality of two maps with the same signature means pointwise equality. Some books identify functions with graphs and treat codomains separately; do not mix conventions mid-proof. The lab requires total functions. A program that raises or diverges needs a model that accounts for those outcomes before it represents such a function.

For R from A to B and S from B to C, S∘R means R first, S second. R+ denotes positive-length reachability; R* also includes zero-length paths and hence all self-pairs. A partial order here is reflexive; its strict part removes self-pairs. The empty set has the empty partition and the empty partial order.

Trees in the lab are finite full binary trees with tagged leaves and nodes. L counts leaves, I counts internal nodes and N counts all node occurrences. L=I+1 depends on every internal node having exactly two children.

A proof-to-code example

To count positive entries in a finite immutable integer list a of length n, use the invariant: after k iterations, 0≤k≤n and c equals the number of positive entries in the prefix a[:k]. Initially k=c=0. One iteration adds one exactly when a[k]>0, so the invariant is preserved after incrementing k. At k=n the prefix is the whole list. The natural-number measure n−k decreases on each iteration, proving termination when each iteration itself terminates.

The proof assumes the list is unchanged during the loop and arithmetic is exact. Python's integers provide exact integer values within available resources; fixed width arithmetic requires overflow reasoning. Neither mathematical termination nor successful finite checks promise that every input fits a real machine.

Countermodel or proof?

A complete truth table proves a propositional identity because all assignments are included. Exhaustively classifying all relations on a three-element carrier checks that finite family. It does not prove the implementation correct for every carrier size. A violating tuple can disprove a relation property immediately, provided it belongs to the declared carrier and satisfies the required premises.

Use guided labs for executable definitions and assessment for independent proof and transfer obligations.