Problem Specifications and Evidence Contracts
Write the contract before evaluating correctness
Record input domain, permitted outputs, invalid-input policy, tie rules,
mutation policy, termination assumptions and resource boundary. A specification
may accept multiple witnesses. Distinguish [] as a valid empty construction,
None as no solution, and unknown as unfinished search.
Evidence ladder
| Evidence | Supports | Does not establish |
|---|---|---|
| Hand trace | Behavior on the stated case | General correctness |
| Exhaustive enumeration | All inputs in the enumerated finite domain | Inputs outside that domain |
| Differential check | Agreement with an oracle | Independence or correctness of that oracle |
| Metamorphic check | A stated relation between transformed inputs | Every output value |
| Proof | Its conclusion under explicit assumptions | A different implementation or model |
| Benchmark | Measured work in a recorded environment | A universal latency guarantee |
An invariant requires initialisation, preservation and an exit argument. Termination additionally needs a well-founded decreasing measure. A necessary condition need not be sufficient. Report search bounds with negative results.
Offline lab API
Python standard library only; functions must not mutate caller lists or graphs. Use ordinary integers (excluding booleans) for integer inputs.
| Function | Contract |
|---|---|
lower_bound(values, target) | Sorted integer list is a caller precondition; return first index with value >= target, or len(values). Duplicates allowed. |
min_coins(coins, amount) | Positive distinct integer denominations, nonnegative integer amount; return any minimum-length list of coins summing to amount, or None. Empty denominations allowed. Invalid domain raises ValueError. |
reverse_reachable(graph, target) | Finite directed graph as a dict from string vertices to lists of string vertices; every endpoint and target must be a key. Return the set of vertices with a path to target, including target. Invalid graph raises ValueError. |
shrink_failure(values, fails) | Integer list and deterministic total Boolean predicate; initial list must fail or raise ValueError. Return a failing subsequence, 1-minimal under single deletions. Propagate predicate exceptions; do not treat them as the same failure. |
For search and shrinking, finiteness and a visited set or decreasing list length are part of the argument. The reducer can call the predicate quadratically many times; predicate cost and list-copy cost must be counted separately.
Evidence record
For each claim, include artifact path, domain, command or proof, observed result, limitation, assistance used, and a changed-case check. Keep predictions separate from observations. A self-check is not independent review.