Skip to content

Software Quality

Contracts and runtime assertions

A contract attaches preconditions, postconditions, and invariants to a function or interface. A runtime assertion is the same idea expressed inline (assert n > 0). This is Design by Contract in its original, runtime-checked form, from Eiffel (Meyer 1992)1 (Design by Contract is a registered trademark of Eiffel Software): the condition is evaluated as the program runs, and a violation crashes or alerts. That makes the guarantee empirical: a violation is caught if it happens on the inputs production actually sends, but a clean run is evidence, not proof.

Checked this way, a contract fills a slot tests and types leave open: types check shape statically, tests check behavior on inputs the author chose, and a runtime contract checks its condition against whatever inputs production actually sends, failing loudly when one breaks (Wayne 2017)2. The same predicate can instead be proved rather than checked at runtime, a wider space mapped by contracts as specifications. A contract on an internal boundary trusts its caller, where a schema validator on an external boundary distrusts its input; schema and boundary validation covers the untrusted side.

Written or inferred

Most contracts are authored — the developer states the pre- or postcondition. They can also be inferred: dynamic invariant detection runs the program over a test suite, watches the values at each program point, and proposes the invariants that held on every observed run as candidate contracts. Daikon is the classic detector (Ernst et al. 2007)3. The catch is that an inferred invariant captures the behavior the suite exercised, not the behavior the author intended — so the output is a set of candidates to review and prune, not contracts to adopt wholesale.

What it catches

  • Boundary violations at runtime. A caller passing a negative index, an out-of-range argument, a string the function expected to be non-empty. The contract fires on the first violation and names the violated condition.
  • Invariant drift. A class invariant ("the cache size is at most the capacity") that holds in tests but is violated in production.
  • Spec/implementation disagreement. A function whose postcondition was written by the author but whose body does something else; the contract fails in tests or in production, making the disagreement loud.
  • Invariant violations in persisted state. Internal state that no longer satisfies its own invariant when re-read (a serialized cache whose size exceeds capacity, a saved aggregate whose totals no longer reconcile). The contract on the loaded value catches the drift.
  • Health-check failures. Watchdog assertions ("queue depth < 10k") that mean something upstream is wrong and protect downstream systems by failing fast.

On their own, contracts catch nothing outside the conditions the author wrote.

A default is a silenced assertion

A lookup that cannot answer has three options: raise, return a value that means absent, or substitute a default. The third one converts a data-availability failure into a plausible answer. An age lookup falling back to "adult" returns a value every downstream condition accepts, so nothing fires and the wrong answer propagates looking exactly like a right one. The condition worth asserting — this value came from the table — is the one a default removes.

A second field carrying the value's origin restores it. An enricher that emits source: "lookup" | "default" beside the field makes the substitution visible in the record, and the fraction of records carrying a default becomes a quantity monitoring can alert on. The value itself cannot be alerted on, because nothing distinguishes a defaulted one from a correct one. Where the caller can handle absence, modeling it as a sum type — Found<T> | Missing — moves the check to compile time, and the compiler rejects the caller that ignores the missing case.

Tools

Runtime contract tooling spans first-class language support, libraries, and process-level watchdogs. The same predicate can be discharged statically instead, by Dafny, F*, Liquid Haskell, SPARK's proof mode, and others; refinement and dependent types covers the type-checked end.

Languages with first-class contracts

  • Eiffel — the design ancestor. Preconditions, postconditions, and class invariants as language constructs, checked at runtime.
  • D — in/out/invariant blocks; runtime-checked.
  • Ada / SPARK — pre/postconditions checked at runtime under the assertion policy (SPARK can also prove them).

Language additions and libraries

  • JML for Java — contracts as annotations, runtime-asserted by jmlrac (OpenJML also checks them statically).
  • .NET — the base-class-library throw helpers are the guard clause: ArgumentNullException.ThrowIfNull (.NET 6), ArgumentException.ThrowIfNullOrEmpty (.NET 7), ArgumentOutOfRangeException.ThrowIfNegative and ThrowIfZero (.NET 8). CommunityToolkit.Diagnostics supplies a fuller Guard API; Debug.Assert covers internal invariants.
  • icontract (Python), PyContracts — Python decorators for pre/postconditions.

Plain assertions

  • Every mainstream language has assert. Java's assert is disabled by default (-ea to enable); C's assert is a one-liner; Rust's debug_assert! runs in debug builds only. Python's assert is stripped under -O.

Health checks, watchdogs, runtime invariants

  • systemd watchdogs, Kubernetes liveness/readiness probes, Erlang/OTP supervision invariants. The same shape — assert a condition, fail fast on violation — at the process boundary.

When to use, when not

Use:

  • Public APIs and module boundaries. The contract documents the intended use and enforces it.
  • Class invariants that are easy to state but easy to break under refactoring. The cost is a one-line method; the benefit is catching drift the moment it happens.
  • Production assertions for invariants you cannot easily test against (database consistency, queue depth, cache hit invariants). Watchdog-style; fail fast.
  • Refactors of legacy code. Pre/postconditions are the entry-level formalism that fits in any language without a verifier.

Don't:

  • For invariants you don't actually believe. A precondition that the author always weakens to True is dead code.
  • For deserializing data from an untrusted source. That is schema and boundary validation's case: a contract assumes a trusted caller, which deserialized external data is not.
  • In hot paths where the assertion cost is measurable. Use debug_assert!-style flags (Rust, C++ debug builds) or strip them in release.
  • As a substitute for tests. Contracts say what should hold; tests check they hold on chosen inputs. The two compose.
  • As a substitute for types. If the language can express the shape constraint statically, prefer the type.

Evidence

There is no controlled defect-rate evidence for runtime-checked contracts specifically. What exists is a deployment record, not measured numbers.

  • Deployment record. NATS iFACTS, the UK en-route air-traffic system, is about 250 kloc logical and mostly SPARK Ada, and was the most ambitious SPARK project as of 2014 (Chapman and Schanda 2014)4. Contracts are usable and maintainable at that size. Most of the SPARK result is a proof story, not runtime checking, and vendor defect-rate differentials vs C/C++ are not independently verified.
  • What is not evidence. The "50% defect reduction" sometimes quoted for Eiffel has no independent replication: industrial folklore. Eiffel is the design lineage (Meyer 1992)1, and that influence is on vocabulary, not measured defect rates. Formal-methods results that prove a spec (AWS (Newcombe et al. 2015)5, Dafny, Liquid Haskell) are evidence for the proving corner, not for runtime checking.

The recommendation rests on the definitional case, not on numbers: a runtime contract checks a spec that types cannot express and tests only sample, against whatever inputs production actually sends.

Looks alike — Design by Contract vs schema validation

Mechanically identical — evaluate a predicate at runtime and throw — so the mechanism doesn't tell them apart; what's being checked does. Validating untrusted boundary data (an HTTP body, an env var) is validation: a failure is expected and you handle it (a 400). Asserting trusted internal state (balance >= 0, a returned list is sorted) is a contract: a failure is a bug, so it crashes and alerts. The same z.refine(...) is validation on a request body and a contract on an internal invariant.

Same name, different thing — Design by Contract vs contract testing (Pact)

These share only the word contract. A contract here is a runtime predicate inside one component — a precondition, postcondition, or invariant. Contract testing (Pact, consumer-driven) is an integration check at a service boundary: it records the messages a consumer expects and replays them against the provider. Different method, different failure — a broken assertion inside a program versus two services drifting out of agreement.

Oracle: predicate

All four answer the same question — does property P hold? — and differ only in how that answer is obtained, from cheapest-and-weakest to strongest:

  • Runtime contracts — check P during execution, on the inputs you actually run, and crash if it's violated.
  • Property-based testing — check P on many generated inputs; empirical, with no guarantee past what was sampled.
  • Refinement & dependent types — encode P in the type, so the compiler rejects any program that could violate it (sound within what the type can express).
  • Theorem proving — prove P holds for all inputs, ahead of time.

Classification

  • Quality dimensions: Functionality, Reliability.
  • Area: API and module boundaries, data deserialization, class invariants on stateful types, watchdogs and health checks.
  • Guarantee: Empirical — a violation is observed once it happens; absence of violations is evidence, not proof.

Referenced by

References

  1. Meyer, Bertrand. 1992. "Applying 'Design by Contract'." Computer 25 (10): 40–51. https://doi.org/10.1109/2.161279. ↩↩

  2. Wayne, Hillel. 2017. Introduction to Contract Programming. https://www.hillelwayne.com/post/contracts/. ↩

  3. Ernst, Michael D., Jeff H. Perkins, Philip J. Guo, et al. 2007. "The Daikon system for dynamic detection of likely invariants." Science of Computer Programming 69 (1–3): 35–45. https://doi.org/10.1016/j.scico.2007.01.015. ↩

  4. Chapman, Roderick, and Florian Schanda. 2014. "Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK." Interactive Theorem Proving (ITP 2014), 17–26. https://doi.org/10.1007/978-3-319-08970-6_2. ↩

  5. Newcombe, Chris, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. 2015. "How Amazon Web Services Uses Formal Methods." Communications of the ACM 58 (4): 66–73. https://doi.org/10.1145/2699417. ↩