# 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)[^meyer1992] (*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)[^wayne2017a]. The same predicate can instead be *proved* rather than checked at runtime, a wider space mapped by [contracts as specifications](https://quality.stereobooster.com/contracts-as-specifications.md). A contract on an internal boundary trusts its caller, where a schema validator on an external boundary distrusts its input; [schema and boundary validation](https://quality.stereobooster.com/schema-and-boundary-validation.md) 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)[^ernst2007]. 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](https://quality.stereobooster.com/monitoring-and-observability.md) 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](https://quality.stereobooster.com/static-types.md) — `Found | 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](https://dafny.org/), [F\*](https://www.fstar-lang.org/), [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell/), SPARK's proof mode, and others; [refinement and dependent types](https://quality.stereobooster.com/refinement-and-dependent-types.md) covers the type-checked end. ### Languages with first-class contracts - **[Eiffel](https://www.eiffel.org/)** — the design ancestor. Preconditions, postconditions, and class invariants as language constructs, checked at runtime. - **D** — `in`/`out`/`invariant` blocks; runtime-checked. - **Ada / [SPARK](https://github.com/AdaCore/spark2014)** — pre/postconditions checked at runtime under the assertion policy (SPARK can also *prove* them). ### Language additions and libraries - **[JML](https://www.openjml.org/)** 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](https://learn.microsoft.com/en-us/dotnet/communitytoolkit/diagnostics/guard) supplies a fuller `Guard` API; `Debug.Assert` covers internal invariants. - **[icontract](https://github.com/Parquery/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](https://quality.stereobooster.com/schema-and-boundary-validation.md)'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)[^chapman2014]. 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)[^meyer1992], and that influence is on *vocabulary*, not measured defect rates. Formal-methods results that *prove* a spec (AWS (Newcombe et al. 2015)[^newcombe2015], 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. ## Related **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**](https://quality.stereobooster.com/schema-and-boundary-validation.md): 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](https://quality.stereobooster.com/snapshot-testing.md) (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](https://quality.stereobooster.com/property-based-testing.md) — *check* P on many generated inputs; empirical, with no guarantee past what was sampled. - [Refinement & dependent types](https://quality.stereobooster.com/refinement-and-dependent-types.md) — *encode* P in the type, so the compiler rejects any program that could violate it (sound within what the type can express). - [Theorem proving](https://quality.stereobooster.com/theorem-proving.md) — *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 - [Quality dimensions](https://quality.stereobooster.com/quality-dimensions.md) · Quality dimensions - [Effect scope](https://quality.stereobooster.com/effect.md) · The axes - [The axes](https://quality.stereobooster.com/axes.md) · The axes - [Contracts as specifications](https://quality.stereobooster.com/contracts-as-specifications.md) · Methods - [Parallel run](https://quality.stereobooster.com/parallel-run.md) · Methods - [Refinement and dependent types](https://quality.stereobooster.com/refinement-and-dependent-types.md) · Methods - [Schema and boundary validation](https://quality.stereobooster.com/schema-and-boundary-validation.md) · Methods - [Snapshot and approval testing](https://quality.stereobooster.com/snapshot-testing.md) · Methods - [State machines and statecharts](https://quality.stereobooster.com/state-machines.md) · Methods - [Theorem proving](https://quality.stereobooster.com/theorem-proving.md) · Methods - [Verifying concurrency](https://quality.stereobooster.com/concurrency.md) · Methods - [Verifying numerical code](https://quality.stereobooster.com/numbers.md) · Methods - [AI tooling for runtime and production](https://quality.stereobooster.com/ai-runtime.md) · AI - [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI - [Choosing methods](https://quality.stereobooster.com/choosing.md) · Overview ## References [^meyer1992]: Meyer, Bertrand. 1992. "[Applying 'Design by Contract'](https://pages.mtu.edu/~aebnenas/teaching/spring2010/cs3141/readings/meyerPDF.pdf)." *Computer* 25 (10): 40–51. . [^wayne2017a]: Wayne, Hillel. 2017. *[Introduction to Contract Programming](https://www.hillelwayne.com/post/contracts/)*. . [^ernst2007]: Ernst, Michael D., Jeff H. Perkins, Philip J. Guo, et al. 2007. "[The Daikon system for dynamic detection of likely invariants](https://people.csail.mit.edu/cpacheco/publications/daikon-tool-scp2006.pdf)." *Science of Computer Programming* 69 (1–3): 35–45. . [^chapman2014]: Chapman, Roderick, and Florian Schanda. 2014. "[Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK](https://proteancode.com/keynote.pdf)." *Interactive Theorem Proving (ITP 2014)*, 17–26. [https://doi.org/10.1007/978-3-319-08970-6\\\_2](https://doi.org/10.1007/978-3-319-08970-6\_2). [^newcombe2015]: Newcombe, Chris, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. 2015. "[How Amazon Web Services Uses Formal Methods](https://cacm.acm.org/research/how-amazon-web-services-uses-formal-methods/)." *Communications of the ACM* 58 (4): 66–73. .