Contract & Refinement Types

Behavioral guarantees checked before the code ever runs. Typestate systems, refinement types, and design-by-contract annotations (Eiffel-style pre/postconditions, Dafny requires/ensures) ask the compiler to prove that certain behaviors are impossible, not merely unlikely.

Where a type checker answers “do the shapes fit?”, a refinement type answers “can withdraw(amount) ever be called with amount > balance?” — a behavioral claim, discharged at build time.

In practice

A contract check reads like a proof obligation returned unpaid. The diagnostic names the obligation that failed, and usually the related location where it was stated:

Program.dfy(14,4): Error: A precondition for this call could not be
proved on an entry point of this program
Program.dfy(14,17): Related location: This is the precondition that
could not be proved
Program.dfy(9,11): Related location: this is the precondition

Three causes produce the same message, and the fix is different for each: the implementation violates its own contract, the contract is wrong, or the prover needs an intermediate lemma to connect the two. The message alone does not say which. Unlike a test failure, though, the verdict is deterministic: a contract that fails today fails on every machine, and a proof that discharges never flakes. What the message will not hand you is a failing input. Dafny can extract one from the solver with --extract-counterexample, and says in the same breath that it “cannot guarantee that the counterexample it reports provably violates the assertion”, and that the output “should be inspected manually and treated as a hint”. A solver model is not a minimal input and is not always a reachable one.

Response playbook

When a contract fails to discharge:

1. Try to reproduce with a concrete input. If the checker will extract a counter-example, run it before believing it — the model is a hint, not a witness. If it will not, derive a candidate from the failed obligation by hand.
2. Decide whether the implementation or the contract is wrong. A failed proof is a genuine disagreement between two claims the author made, and one of them must be retracted.
3. If both are right, supply the missing lemma. Splitting the obligation into smaller steps is how proofs go through; deleting the contract is how they get abandoned.
4. Demote what cannot be proved. An obligation that resists the prover can still ship as a runtime invariant, checked on every execution instead of all executions.

How it gets gamed

The checker cannot be gamed, but the contracts are written by the same mind that writes the code, so the specification itself can be degraded:

• Trivial contracts. ensures true, postconditions that restate the type signature. The checker passes and protects nothing.
• Weaken until green. Each fight loosens the precondition one notch until the proof goes through by erosion rather than by correctness.
• Verification off the merge path. A proof job that runs nightly or on demand, rather than on every merge, is a proof nobody is waiting for.

The meta-signal is contract strength: sample annotated functions and count how many have postconditions that are trivially true.

What it cannot detect

Contracts only cover what was specified. The specification itself is written by the same mind that wrote the code, which is why contract checking composes with rather than replaces example-based tests and property testing.

Related sensors

References

Publications

• How Amazon Web Services Uses Formal Methods — Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff · 2015 · case study · Communications of the ACM 58(4)
• Dafny: An Automatic Program Verifier — Leino · 2010 · argument

Tooling

• DafnyVerification-aware programming language
• Frama-CStatic analysis and verification for C
• JMLJava Modeling Language for behavioral interface specifications
• Rust typestateRust's type system encoding program states

Further reading

• Dafny user guide, verification debugging