Bond (Design by Contract for Elixir) - 1.14 released

Bond brings Design by Contract to Elixir: preconditions, postconditions and invariants as executable specifications, checked at runtime and compiled out of production if you want them gone.

The last update here covered 1.8.0 and Bond.Server. Six minor releases have landed since, so rather than post each one I’ve batched them. Everything below is in 1.14.1, out now on Hex.

Destructuring bindings in contracts: where and whenever (1.10.0)

<~ matches a pattern, but the names it binds are trapped — you can only constrain them with a when guard, and guards are a closed sublanguage: no forall/exists, no function calls, no comparisons against computed values. So asserting something about a list nested inside a map inside a tuple meant giving up either the destructuring or the assertion.

where and whenever bind a pattern and scope Bond’s full assertion syntax to the names it introduces:

@post whenever({:ok, %{urls: urls}} <- result),
      non_empty: urls != [],
      all_https: forall(u <- urls, String.starts_with?(u, "https"))
def fetch(source), do: ...

The keyword picks the semantics and the arrow reinforces it. where uses = — the value is this shape, and a mismatch is a violation, exactly like = raising a MatchError. whenever uses <- — the value might match, and a mismatch is vacuously satisfied, like a with generator. Because whenever is vacuous on a non-match, case analysis is one clause per shape with no or {:error, _} boilerplate:

@post whenever({:ok, payload} <- result), valid: valid?(payload)
@post whenever({:error, reason} <- result), known: reason in [:timeout, :refused]

Each scoped assertion keeps its own label, so a failure pinpoints the shape and the constraint:

** (Bond.PostconditionError) postcondition failed in Session.fetch/1
|   label: :all_https
|   assertion: forall(u <- urls, String.starts_with?(u, "https"))
|   counterexample: element at index 1 ("http://nope") does not satisfy `String.starts_with?(u, "https")`
|   binding: [result: {:ok, %{urls: ["https://a", "http://nope"]}}, urls: [...]]

Available in @pre, @post, @invariant, Bond.Server’s @state_invariant / @transition_invariant, inherited contracts on Bond.Behaviour callbacks and Bond.Protocol functions, the qualified Bond.pre/Bond.post forms, and check/1.

A compile-time linter for assertions that can’t fail (1.11.0)

A contract that can never fail protects nothing but reads as coverage — worse than no contract, because a missing contract is honestly silent and a vacuous one lies. Bond now warns at compile time when it can prove an assertion is constant:

warning: Bond assertion linter: `x == x` compares a term with itself and is always `true` —
did you mean to compare two different values?

warning: Bond assertion linter: `forall(i <- items, true)` has a constant predicate (`true`),
so the `forall` only tests whether the enumerable is empty.

The ruleset is deliberately narrow — constant folding over literals, self-comparisons, and vacuous quantifiers — because a noisy contract linter is one you turn off. It does not attempt type-disjoint comparisons over runtime variables (key not in remaining_keys where the two can never be equal), which needs inference Bond doesn’t do. Disable with config :bond, lint_assertions: false.

Related fix in the same release: a forall/exists whose generator uses a structural pattern (forall(%{retry: r} <- entries, r >= 0)) used to raise FunctionClauseError on any element that didn’t match. It now fails cleanly with a counterexample naming the unmatched pattern — so a destructuring generator doubles as a shape assertion, as the syntax suggests.

Property-testing a GenServer through its reachable states (1.12.0)

1.8.0 added Bond.Server, which checks @state_invariant and @transition_invariant around a server’s callbacks. The obvious next question is how you exercise those invariants, and hand-writing a state generator answers it badly — you end up testing the states you thought of, and drifting out of sync with the server.

server_invariants_hold/2 generates random message sequences instead, drives the server through them, and lets the invariants be the oracle across states the server can actually reach:

server_invariants_hold Bank,
  init: StreamData.integer(0..100),
  messages: [
    call: [{:withdraw, [StreamData.positive_integer()]}, {:balance, []}],
    cast: [{:deposit, [StreamData.integer(1..2_000)]}],
    info: [{:tick, []}]
  ]

There’s no model to write and keep in step — the contracts already say what must hold. A violation shrinks to a minimal (init, sequence) counterexample:

** (ExUnitProperties.Error) failed with generated values (after 5 successful runs):

    * Clause:    init_arg <- StreamData.integer(0..100)
      Generated: 13
    * Clause:    ops <- sequence_gen
      Generated: [cast: {:deposit, 1884}]

got exception:

    ** (Bond.InvariantError) transition invariant violated across Bank.handle_cast/2
    |   label: :no_free_money
    |   assertion: new_state.balance <= old_state.balance + 1000
    |   binding: [new_state: %{balance: 1897}, old_state: %{balance: 13}]

Two modes: :callbacks (default) invokes callbacks directly, threading each returned state into the next — fast, deterministic, quiet, and the right default for CI. :process starts a real server and drives it with GenServer.call/cast/send, for when dispatch or timer behaviour is part of what you’re testing.

1.9.0 also extended probe_contract/2 (from 1.7.0) to probe size boundaries: a @pre length(items) <= 3 now gets exercised with length-2/3/4 lists built from your generator’s own output, rather than being filter-only.

Named contracts, finished (1.13.0)

1.5.0 introduced defcontract/@apply_contract and 1.6.0 added include for composing them. Three gaps are now closed:

Result-only contracts work across functions of different arities. Declare with an explicit empty parameter list and the contract becomes arity-agnostic:

defcontract gate_result() do
  @post {:ok, :cleared} <~ result
end

@apply_contract :gate_result
def can_encode?(game_film), do: ...            # arity 1

@apply_contract :gate_result
def can_encode?(game_film, exchange_file), do: ...   # arity 2

defcontract and @apply_contract now work inside Bond.Behaviour and Bond.Protocol declaration modules, so an abstraction can name a shared agreement once and reference it from several callbacks. Implementers see no difference.

A zero-arg contract can be applied to an @impl function that already inherits a behaviour contract — the applied postconditions are added alongside the inherited ones, equivalent to @post_strengthen but named and reusable.

“The contract is false” vs. “the contract couldn’t be evaluated” (1.14.0)

Those are different facts, and Bond used to conflate them. An assertion that raises rather than returning true or false now gets its own error:

@pre valid: String.contains?(email, "@")
def normalize(email), do: String.downcase(email)

normalize(nil)
** (Bond.AssertionEvaluationError) precondition could not be evaluated for call to MyApp.normalize/1
|   label: :valid
|   assertion: String.contains?(email, "@")
|   binding: [email: nil]
|   raised: ** (FunctionClauseError) no function clause matching in String.contains?/2

This matters more than it looks. A partial assertion is the one case where turning contracts on changes behaviour rather than just adding a check — it can turn a call that would have worked into a raise, and :purge makes it disappear again. Naming it as its own failure mode makes that visible instead of surfacing a bare FunctionClauseError from inside your predicate with nothing connecting it to Bond. The fix is usually to lead with a type check: is_binary(email) and String.contains?(email, "@").

Also new: Bond warns when a public function’s precondition calls a private function. A precondition is an obligation on the caller, so a caller that can’t evaluate it can’t discharge it — and Bond renders the assertion into your generated docs, where the private helper doesn’t appear. That’s Meyer’s Precondition Availability rule (OOSC §11.7), which Eiffel enforces as a language rule. Postconditions are exempt: they’re the function’s promise, not the caller’s obligation. Suppressible per function, per module, or globally.

Upgrade note: invariants that were being skipped now fire

1.14.0 fixed three separate defects that silently skipped @invariant checks Bond documented as running — including a head that names the struct without binding it, and a struct nested inside a tuple in the head. If you use @invariant and upgrade from 1.8.0, expect invariants to start firing on functions where they previously didn’t. That’s the intended behaviour, but it can surface existing violations, so it’s worth upgrading somewhere you can watch.

Also fixed in 1.13.1: @doc was being discarded on functions Bond doesn’t wrap, and use Bond, at_annotations: false could overwrite documentation. And Bond.Server no longer wraps functions that merely share a name and arity with a GenServer callback in a non-GenServer module.

Documentation (1.14.1)

The most recent release is documentation only. There’s now a cheatsheet — every form Bond provides on one scannable page — and the guides have been reorganised so the reference material lives in the reference guide rather than in the tutorial. The sidebar is grouped into Guides / Reference / About.

Three corrections worth naming, since they were wrong rather than merely unclear: the public API page didn’t list Bond.Config (the runtime toggle API the guides reference throughout), one guide promised a “locking pattern” that no guide contained, and the overhead guide claimed a runtime-disabled contract costs “roughly half” of an enabled one — measured, it’s 7–30% depending on the kind. The overhead numbers are now medians across repeated runs rather than single runs.

Feedback welcome

Bond is at 1.14.1 with the API stable under semver — the Public API surface page enumerates exactly what that covers. If you try it and something is awkward, an issue or a reply here is genuinely useful; a good deal of what’s above started as someone pointing out a rough edge.

Links