View Source What Should a Contract Say?

Bond gives you the syntax for writing assertions and no opinion about what to put in them. This guide is about that question — not whether an assertion is sound (the next guide covers that), but what it should be saying in the first place.

The short answer: a contract states what a function promises. Catching bugs is what that does when an implementation disagrees with its promise, which is a consequence worth having but not the purpose.

That distinction sounds academic and is not. It changes which contracts get written, and how many.

How much to contract

The default is yes. Aim for a contract on every non-trivial function, and read the rest of this guide — and the soundness one — as a quality bar on the assertion you are about to write rather than as a gate to argue past before writing one.

That needs saying, because the failure mode here is one-sided and invisible. A codebase with too few contracts looks exactly like a codebase that never needed them: nothing is missing, nothing is red, and the functions that quietly promise nothing look the same as the functions that have nothing to promise. Careful screening under-contracts by default, and the shortfall never announces itself.

One measurement, from a Phoenix application contracted with these guides: 67 of its 126 source files use Bond, between them carrying 136 postconditions, 28 preconditions and 13 struct invariants across 12 struct modules — and its author's assessment was that reaching that point took five passes, because every earlier one stopped too early.

The near five-to-one ratio of postconditions to preconditions is the part worth internalising. Most functions have something to promise; far fewer have something to demand. If you go looking for a @pre and come up empty, that is the normal case, not a signal to move on — ask what the function returns instead, which is where the interesting laws live.

None of this lowers the bar. An assertion that restates mechanism, cannot be evaluated, or accuses correct code is worse than none, and everything that follows still applies. What changes is the presumption: contract it unless one of the stated reasons applies.

The instruction is prescriptive; the assertion is descriptive

Meyer puts it directly. A stack's full? has an obvious implementation, and a postcondition that appears to say the same thing:

@post definition: result == (stack.count == stack.capacity)
def full?(%__MODULE__{} = stack), do: stack.count == stack.capacity

The natural reaction is that the postcondition is redundant — the body already says it, with = in place of ==. It is not:

The instruction is prescriptive; the assertion is descriptive. The instruction describes the "how"; the assertion describes the "what". The instruction is part of the implementation; the assertion is an element of specification.

— Object-Oriented Software Construction, 2nd edition, §11.7, p. 352

The body is a command: compute this. The assertion is a claim about the end state that a caller can rely on without reading the body. They resemble each other here only because the implementation is trivial, and Elixir's == looks like Eiffel's =.

Meyer answers the obvious objection — that a plausible rewrite could never violate it — on its own terms. The body could just as well have been:

def full?(%__MODULE__{} = stack) do
  if stack.count == stack.capacity, do: true, else: false
end

The postcondition is what says those two are the same function. And the resemblance is an artefact of the example being one line. Meyer's own next case is a square root, whose postcondition is abs(Result ^ 2 - x) <= tolerance — nothing about which looks like an algorithm for computing square roots:

@post within_tolerance: abs(result * result - x) <= 1.0e-9
def sqrt(x), do: # ... Newton-Raphson, or whatever you like

Same specification, wildly different implementation. That is the normal case; full? is the degenerate one.

The test is mechanism versus meaning

"Does the assertion restate the body?" is the wrong question, because for a short function the answer is often yes and the contract is still worth having. The question that holds up is whether the assertion describes mechanism or meaning.

# ❌ Mechanism. This is the implementation, spelled twice.
@post mapped: result == Enum.map(xs, &transform/1)
def process(xs), do: Enum.map(xs, &transform/1)

# ✅ Meaning. It happens to fit on one line, but it is a claim about the
#    result, not a recipe for producing it.
@post definition: result == (stack.count == stack.capacity)
def full?(%__MODULE__{} = stack), do: stack.count == stack.capacity

The first names the algorithm — Enum.map over xs applying transform/1. Change the implementation to a for comprehension or a Stream and you must change the assertion in the same edit, because the assertion is the implementation.

The second names a property. It survives any rewrite of full? that remains correct, which is precisely what you want a specification to do.

A useful sharpening: if you cannot describe the assertion without describing how the function works, it is mechanism.

A one-line implementation still deserves a specification

The strongest argument against discarding full?'s postcondition is that Bond publishes it.

Bond generates #### Preconditions and #### Postconditions sections into ExDoc from your contracts — Eiffel's short form, the view of a class with implementations stripped out and only the specification left. That is what makes it reasonable to treat a contract as the published interface rather than an internal test aid.

A postcondition that mirrors a one-line body still tells every reader of the docs what the function guarantees, without asking them to read the source. Most of its value is delivered before anything runs.

So "delete it, it can never fail" trades a published specification for nothing. If the assertion states meaning rather than mechanism, keep it.

A delegating body still owes its caller the guarantee

The same trap has a third form, one altitude up. A function whose body hands the work to a collaborator that already guarantees a property looks like it has nothing left to promise:

# The mapper's own @post already guarantees this. State it here anyway.
@post both_halves_usable: forall(ref <- result, usable?(ref))
def playlist_item_references(client, id, opts) do
  client |> fetch_pages(id, opts) |> Mapper.references()
end

"The mapper already checks it" describes how this function is built today. It is mechanism — and a refactor can retire that mapper next month without touching what this function promises. The guarantee is the specification: it renders into this function's generated docs, and its callers read it there, with no reason to know the mapper exists.

It shows up while mutation testing, wearing a disguise: mutate the mapper and the mapper's own postcondition raises first, one call inward, so the outer contract never sees the bad value and looks unfalsifiable. It isn't — see Running a mutation for how to aim at the right function.

Well-behaved callers are not a reason to skip a contract

The same mistake has a second form, which looks at the callers rather than the body:

Every caller of withdraw/2 checks the balance first, and two of them have contracts of their own saying so. A @pre here could never fire.

It could never fire today. A precondition is not a claim about the call sites that happen to exist when you write it — it is a standing obligation on every call site that will ever exist:

@pre sufficient_funds: amount <= account.balance
def withdraw(%Account{} = account, amount)

And call sites arrive: a new feature, a refactor that routes an old path somewhere new, a second application once the module ships as a library. Nothing else in the codebase meets that eleventh caller. The other ten callers' contracts constrain them; they say nothing about withdraw/2, and they stop covering anything the moment somebody adds a caller without reading them.

So the reasoning runs the other way round. Careful callers are why this row will read ⚠ never failed in the coverage table for a year — not a reason to leave it unwritten. The day it does fire, it names the caller that got it wrong, at the call, instead of letting a negative balance travel somewhere it will be much harder to explain.

The same holds for a supplier: a @post is not made redundant by an implementation that currently satisfies it. Satisfying it is the normal state. The contract is what tells you the day that changes.

Three questions

When you are unsure what to write, these are usually enough:

What must the caller guarantee for this call to make sense? That is the @pre. Not "what would crash the body" — what the specification requires. A precondition you cannot justify from the function's stated purpose is usually the implementer's convenience leaking into the interface.

What does this function promise in return? That is the @post. State it as a property of result — and of the arguments, and of old(...) state where something changed. If the honest answer is "whatever the body computes", there is nothing to say and you should say nothing.

What is always true of this value, between calls? That is the @invariant. It belongs to the type rather than to any one function, and Bond checks it around every public function of the declaring module.

Where soundness comes in

Everything above is about what a contract means. Whether it works — whether it can actually fail on the input it is meant to reject, whether it is total, whether it says what it appears to say — is a separate question, and a large one.

Falsifiability is how you check an assertion is good. Stating the specification is why you write one. Both matter; they are not the same test, and applying the first as though it were the second is how correct specifications get deleted.

Writing Sound Assertions is the next guide, and covers the second question in full.

See also