A contract is a predicate on an interface — what an operation requires of its caller, and what it guarantees in return. The requirement is a precondition, the guarantee a postcondition, and a predicate that holds throughout is an invariant. This is Hoare's idea (Hoare 1969)¹: the triple $\{P\}\,c\,\{Q\}$ reads "if $P$ holds and $c$ runs, $Q$ holds after". It assumes no paradigm and no moment of enforcement. The operation can be a function, a procedure, a method, or a module boundary; the predicate can be checked as the program runs or proved before it ever does. Stripped to that, a contract is a precondition/postcondition pair on an interface.

The word "specification" also names a nearby method. An executable specification is a spec that is run: a second, deliberately obvious implementation used as a differential reference oracle, whereas a contract predicate is asserted or proved.

One predicate, several roles

The predicate is the atom. $x > 0$, or "the list is sorted", is a boolean function of a value; everything the literature calls by a grander name is that atom placed somewhere or discharged some way:

• Position — checked on entry (a precondition), on exit (a postcondition), or held before and after every operation on some state (an invariant): a loop, a data structure, a module, or an object.
• Kind — a shape the value must have, which is exactly a type ($x : T$); or a richer predicate a type cannot state ($x > 0$, "the list is sorted"). Schema validation is the shape case applied to boundary data.
• Discharge — when and how the predicate is established: checked at runtime and crashed on, proved at compile time by an SMT solver, or proved by hand as part of the type.

A type, a refinement type, a property test, a schema validator, and a runtime contract are the same predicate at different points of this space. ("Invariant" itself carries three different meanings across these roles; the glossary separates them.)

The same condition, across languages

Thirteen systems that attach predicates to code, grouped by how they discharge the predicate. The columns are the capabilities beyond the bare predicate.

Runtime-checked

The condition is evaluated as the program runs; a violation crashes or alerts.

System (paradigm)	invariant	termination	framing	refinement / dependent	discharge	guarantee
Eiffel (OO)	primitive	loop variant	—	—	runtime check	empirical
assert / icontract (Python)	—	—	—	—	runtime check	empirical

Specification languages (discharge-agnostic)

One specification, written once; a separate back-end either checks it at runtime or proves it statically.

System (paradigm)	invariant	termination	framing	refinement / dependent	discharge	guarantee
JML (Java)	primitive	loop variant	assignable	—	runtime or SMT	empirical / sound
Frama-C / ACSL (C)	type inv.	terminates	assigns	—	SMT/proof or runtime	empirical / sound
SPARK (Ada)	type inv.	loop variant	Global	subtype pred.	GNATprove + flow + runtime	sound / empirical
GOSPEL (OCaml)	type inv.	variant	modifies	—	Ortac runtime, Cameleer SMT, or proof	empirical / sound

Language-integrated provers (static)

The prover is part of the language; the compiler discharges every predicate before the program runs.

System (paradigm)	invariant	termination	framing	refinement / dependent	discharge	guarantee
Dafny	idiom (Valid())	decreases	reads/modifies	subset types	SMT (Z3)	sound
F* (FP + dependent)	refinement	decreases	effect + modifies	refinement + dependent	SMT + tactics	sound → mathematical
Liquid Haskell (FP)	— (measures)	built-in	n/a (pure)	refinement	SMT	sound
Verus (Rust)	idiom (spec fn)	decreases	via ownership	—	SMT + proof code	sound
Prusti (Rust)	primitive	not a focus	via ownership	—	SMT (Viper)	sound (safety)
Coq / Agda / Lean	indexed types	total by default	n/a (pure)	full dependent	proof term	mathematical
Idris (dependent PL)	indexed types	opt-in	n/a (pure)	full dependent	proof term	mathematical if total

The only universal is the precondition/postcondition pair. It is the one capability all thirteen systems share, across object-oriented, functional, systems, and dependently typed languages. Even where there is no requires/ensures clause, the pair is present: in the dependent-type systems the precondition is a function argument and the postcondition the return type. Invariants are sometimes a keyword, sometimes a hand-written predicate, sometimes absent; framing, termination, and refinement are each missing somewhere.

Framing and termination are the price of proving, not features of contracts. The runtime-checked systems have neither a framing clause nor a termination metric; every system that proves statically has both. A frame clause (reads/modifies/assigns) exists only so a modular proof can conclude that a call left everything else untouched; a termination metric (decreases/variant) exists only to rule out a non-terminating body that would satisfy any postcondition vacuously. A runtime check simply executes and crashes on violation — it needs neither the frame nor a termination proof. The exceptions confirm the mechanism: Prusti is a static prover that omits termination because its goal is panic-freedom rather than totality, and Idris makes totality opt-in because it is built to be a practical programming language.

The columns compress to two axes the project already has. Strip the induced machinery and what remains are two independent dials: discharge (runtime check → SMT → interactive proof) and expressiveness (shape → value predicate → refinement → dependent type). The first is the guarantee axis — runtime check yields an empirical claim, SMT an exhaustive one, a proof assistant a mathematical one. The second is the shape-vs-richer-predicate split already drawn on the refinement and dependent types page. Every system is a point in this plane: a bare assert sits at value-predicate × runtime, F* at dependent × mathematical (Swamy et al. 2016)².

Framing is aliasing debt, and purity or ownership pre-pays it. The framing column splits three ways, tracking how much the language already constrains aliasing. A pure language (Liquid Haskell (Vazou et al. 2014)³) needs no frame because there is no mutable heap. An ownership language gets the frame from its type system — Verus and Prusti both read Rust's borrow checker, which already bounds aliasing, so a hand-written modifies is largely unnecessary. Everywhere else — Dafny (Leino 2010)⁴, ACSL, JML, SPARK, GOSPEL, F* — the frame is paid by hand.

Whether the invariant is a keyword is a design choice, not a necessity. The invariant column splits between systems that offer a primitive invariant (Eiffel, JML, Prusti) and systems where the invariant is an ordinary predicate written by hand — Dafny's Valid() over a Repr set, a Verus spec function — threaded through requires/ensures. The cleanest evidence that this is taste rather than necessity is that Verus and Prusti target the same language and chose oppositely. A class invariant is, mechanically, a predicate conjoined to the pre- and postcondition of every public operation; a language can surface that as sugar or leave it to the author.

Information flow is the one thing a contract cannot state. SPARK's Depends clause (Chapman and Schanda 2014)⁵ is the one capability no other system in the table carries: it specifies which inputs influence which outputs — a non-interference property. That is not a Hoare triple over one run; it is a hyperproperty, a relation over two or more executions, the same shape as a metamorphic relation on the oracle axis (Chen et al. 2018; Barr et al. 2015)^{6 7}. A contract predicate judges a single execution, which is why only one system carries flow and why SPARK discharges it with a separate flow analysis rather than its contract engine.

Design by Contract is one corner of this

"Contract" is Meyer's word, and Design by Contract is the narrower tradition it comes from (Meyer 1992)⁸: assertions checked at runtime, anchored in object-oriented classes, with the class invariant as the defining construct (Design by Contract is a registered trademark of Eiffel Software). Seen only through that lens a contract looks like an assert with ceremony, and mechanically a runtime-checked one is exactly that. Both traits are choices, not the essence: the precondition/postcondition pair is Hoare's, predates objects, and holds for a C function or an SMT proof obligation with no class in sight.

Contracts and runtime assertions is the runtime-checked corner as a method of its own, the cheapest point on the discharge axis. Its higher-order generalization, where a contract guards a function passed as a value, requires genuine machinery to assign blame (Findler and Felleisen 2002)⁹; the weakest-precondition account that lets F* and Dafny prove the same triples rather than check them is the Dijkstra-monad construction (Ahman et al. 2017)¹⁰. What a contract is, in any one system, is a predicate placed at a position, of some kind, discharged some way.

Related

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.

Referenced by

• The axes · The axes
• Contracts and runtime assertions · Methods
• Formal methods · Methods
• Termination analysis · Methods
• Glossary · Overview

References

---

1. Hoare, C. A. R. 1969. "An Axiomatic Basis for Computer Programming." Communications of the ACM 12 (10): 576–80. https://doi.org/10.1145/363235.363259. ↩

2. Swamy, Nikhil, Cătălin Hriţcu, Chantal Keller, et al. 2016. "Dependent Types and Multi-Monadic Effects in F*." Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '16), 256–70. https://doi.org/10.1145/2837614.2837655. ↩

3. Vazou, Niki, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. "Refinement Types for Haskell." Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP '14), 269–82. https://doi.org/10.1145/2628136.2628161. ↩

4. Leino, K. Rustan M. 2010. "Dafny: An Automatic Program Verifier for Functional Correctness." Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16), Lecture notes in computer science, vol. 6355: 348–70. https://doi.org/10.1007/978-3-642-17511-4_20. ↩

5. 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. ↩

6. Chen, Tsong Yueh, Fei-Ching Kuo, Huai Liu, et al. 2018. "Metamorphic Testing: A Review of Challenges and Opportunities." ACM Computing Surveys 51 (1): 1–27. https://doi.org/10.1145/3143561. ↩

7. Barr, Earl T., Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo. 2015. "The Oracle Problem in Software Testing: A Survey." IEEE Transactions on Software Engineering 41 (5): 507–25. https://doi.org/10.1109/TSE.2014.2372785. ↩

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

9. Findler, Robert Bruce, and Matthias Felleisen. 2002. "Contracts for Higher-Order Functions." Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), 48–59. https://doi.org/10.1145/581478.581484. ↩

10. Ahman, Danel, Cătălin Hriţcu, Kenji Maillard, et al. 2017. "Dijkstra Monads for Free." Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '17), 515–29. https://doi.org/10.1145/3009837.3009878. ↩