# Contracts as specifications

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)[^hoare1969]: 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](https://quality.stereobooster.com/executable-specifications.md) 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](https://quality.stereobooster.com/glossary.md) 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](https://www.eiffel.org/) (OO) | primitive | loop variant | — | — | runtime check | empirical |
| `assert` / [icontract](https://github.com/Parquery/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](https://www.openjml.org/) (Java) | primitive | loop variant | `assignable` | — | runtime *or* SMT | empirical / sound |
| [Frama-C](https://www.frama-c.com/) / ACSL (C) | type inv. | `terminates` | `assigns` | — | SMT/proof *or* runtime | empirical / sound |
| [SPARK](https://github.com/AdaCore/spark2014) (Ada) | type inv. | loop variant | `Global` | subtype pred. | [GNATprove](https://docs.adacore.com/spark2014-docs/html/ug/) + flow + runtime | sound / empirical |
| [GOSPEL](https://github.com/ocaml-gospel/gospel) (OCaml) | type inv. | `variant` | `modifies` | — | [Ortac](https://github.com/ocaml-gospel/ortac) runtime, [Cameleer](https://github.com/ocaml-gospel/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](https://dafny.org/) | idiom (`Valid()`) | `decreases` | `reads`/`modifies` | subset types | SMT ([Z3](https://github.com/Z3Prover/z3)) | sound |
| [F\*](https://www.fstar-lang.org/) (FP + dependent) | refinement | `decreases` | effect + `modifies` | refinement + dependent | SMT + tactics | sound → mathematical |
| [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell/) (FP) | — (measures) | built-in | n/a (pure) | refinement | SMT | sound |
| [Verus](https://github.com/verus-lang/verus) (Rust) | idiom (spec fn) | `decreases` | via ownership | — | SMT + proof code | sound |
| [Prusti](https://github.com/viperproject/prusti-dev) (Rust) | primitive | not a focus | via ownership | — | SMT (Viper) | sound (safety) |
| [Coq](https://rocq-prover.org/) / [Agda](https://github.com/agda/agda) / [Lean](https://lean-lang.org/) | indexed types | total by default | n/a (pure) | full dependent | proof term | mathematical |
| [Idris](https://www.idris-lang.org/) (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](https://github.com/viperproject/prusti-dev) is a static prover
that omits termination because its goal is panic-freedom rather than totality,
and [Idris](https://www.idris-lang.org/) 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](https://quality.stereobooster.com/guarantee.md) — 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](https://quality.stereobooster.com/refinement-and-dependent-types.md) page.
Every system is a point in this plane: a bare `assert` sits at value-predicate ×
runtime, [F\*](https://www.fstar-lang.org/) at dependent × mathematical (Swamy et al. 2016)[^swamy2016].

**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](https://ucsd-progsys.github.io/liquidhaskell/) (Vazou et al. 2014)[^vazou2014])
needs no frame because there is no mutable heap. An ownership language gets the
frame from its type system — [Verus](https://github.com/verus-lang/verus) and [Prusti](https://github.com/viperproject/prusti-dev) both
read Rust's borrow checker, which already bounds aliasing, so a hand-written
`modifies` is largely unnecessary. Everywhere else — [Dafny](https://dafny.org/)
(Leino 2010)[^leino2010], ACSL, JML, SPARK, [GOSPEL](https://github.com/ocaml-gospel/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](https://github.com/verus-lang/verus) and [Prusti](https://github.com/viperproject/prusti-dev) 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)[^chapman2014] 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](https://quality.stereobooster.com/metamorphic-testing.md)
on the [oracle axis](https://quality.stereobooster.com/oracle.md) (Chen et al. 2018; Barr et al. 2015)[^chen2018] [^barr2015]. 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)[^meyer1992]: 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](https://quality.stereobooster.com/contracts-and-runtime-assertions.md)
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)[^findler2002]; 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)[^ahman2017]. 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](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.

## Referenced by

- [The axes](https://quality.stereobooster.com/axes.md) · The axes
- [Contracts and runtime assertions](https://quality.stereobooster.com/contracts-and-runtime-assertions.md) · Methods
- [Formal methods](https://quality.stereobooster.com/formal.md) · Methods
- [Termination analysis](https://quality.stereobooster.com/termination-analysis.md) · Methods
- [Glossary](https://quality.stereobooster.com/glossary.md) · Overview

## References

[^hoare1969]: Hoare, C. A. R. 1969. "[An Axiomatic Basis for Computer Programming](https://web.stanford.edu/class/cs357/hoare69.pdf)." *Communications of the ACM* 12 (10): 576–80. <https://doi.org/10.1145/363235.363259>.
[^swamy2016]: Swamy, Nikhil, Cătălin Hriţcu, Chantal Keller, et al. 2016. "[Dependent Types and Multi-Monadic Effects in F\*](https://hal.science/hal-01265793/document)." *Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '16)*, 256–70. <https://doi.org/10.1145/2837614.2837655>.
[^vazou2014]: Vazou, Niki, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. "[Refinement Types for Haskell](https://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pdf)." *Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP '14)*, 269–82. <https://doi.org/10.1145/2628136.2628161>.
[^leino2010]: Leino, K. Rustan M. 2010. "[Dafny: An Automatic Program Verifier for Functional Correctness](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml203.pdf)." *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](https://doi.org/10.1007/978-3-642-17511-4\_20).
[^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).
[^chen2018]: Chen, Tsong Yueh, Fei-Ching Kuo, Huai Liu, et al. 2018. "[Metamorphic Testing: A Review of Challenges and Opportunities](https://www.cs.hku.hk/data/techreps/document/TR-2017-04.pdf)." *ACM Computing Surveys* 51 (1): 1–27. <https://doi.org/10.1145/3143561>.
[^barr2015]: Barr, Earl T., Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo. 2015. "[The Oracle Problem in Software Testing: A Survey](https://ieeexplore.ieee.org/ielx7/32/7106034/06963470.pdf)." *IEEE Transactions on Software Engineering* 41 (5): 507–25. <https://doi.org/10.1109/TSE.2014.2372785>.
[^meyer1992]: Meyer, Bertrand. 1992. "[Applying 'Design by Contract'](https://pages.mtu.edu/~aebnenas/teaching/spring2010/cs3141/readings/meyerPDF.pdf)." *Computer* 25 (10): 40–51. <https://doi.org/10.1109/2.161279>.
[^findler2002]: Findler, Robert Bruce, and Matthias Felleisen. 2002. "[Contracts for Higher-Order Functions](https://www2.ccs.neu.edu/racket/pubs/icfp2002-ff.pdf)." *Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02)*, 48–59. <https://doi.org/10.1145/581478.581484>.
[^ahman2017]: Ahman, Danel, Cătălin Hriţcu, Kenji Maillard, et al. 2017. "[Dijkstra Monads for Free](https://arxiv.org/pdf/1608.06499)." *Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '17)*, 515–29. <https://doi.org/10.1145/3009837.3009878>.

## Acronyms

- ACSL — ANSI/ISO C Specification Language
- FP — functional programming
- PL — programming languages (the research field)
- SMT — satisfiability modulo theories