View Source Bond (Bond v1.14.0)

Design by Contract for Elixir.

A contract is a plain Elixir expression attached to a function and checked at runtime. Here is one that says money is neither created nor destroyed:

defmodule Account do
  defstruct [:owner, :balance]
end

defmodule Ledger do
  use Bond

  @pre sufficient_funds: amount <= from.balance
  @post conserved: result.from.balance + result.to.balance == from.balance + to.balance
  def transfer(%Account{} = from, %Account{} = to, amount) do
    %{
      from: %{from | balance: from.balance - amount},
      to: %{to | balance: to.balance + amount}
    }
  end
end

@pre declares a precondition — what the caller must satisfy for the call to be valid. @post declares a postcondition — what the function promises in return, provided the precondition held. A postcondition can mention result, the function's return value, which a when guard cannot do at all. (Guards keep the jobs only they can do — dispatch, and standing in for types — see Should I remove guards when I add contracts?.)

Note what conserved is not: a restatement of the body. The body moves money; the contract states the law the movement must obey. So when someone later adds a transfer fee and takes it out of the sender only, the arithmetic still looks plausible — and the contract fails:

# Ledger.transfer(ana, bo, 200)   # after a 1% fee is deducted from the sender
** (Bond.PostconditionError) postcondition failed in Ledger.transfer/3
|   at: lib/ledger.ex:9
|   label: :conserved
|   assertion: result.from.balance + result.to.balance == from.balance + to.balance
|   binding: [
  amount: 200,
  from: %Account{owner: "ana", balance: 1000},
  result: %{
    to: %Account{owner: "bo", balance: 250},
    from: %Account{owner: "ana", balance: 798}
  },
  to: %Account{owner: "bo", balance: 50}
]

The failure names the property that broke, and hands you both states to compare.

Beyond preconditions and postconditions

@pre and @post constrain one call at a time. The rest of Bond is about getting more out of the same statements — enforcing them across a whole module, across every implementation of a behaviour, and against inputs you never wrote down.

Checked at every entrance and exit of a module. An @invariant is a property of the struct rather than of any one call, so Bond checks it around every public function — including the ones a colleague adds next year:

defmodule Cart do
  use Bond

  defstruct items: [], total_cents: 0

  @invariant total_matches_items:
               subject.total_cents == Enum.sum(Enum.map(subject.items, & &1.cents))

  @post added_one: length(result.items) == length(cart.items) + 1
  def add_item(%Cart{} = cart, item) do
    %{cart | items: [item | cart.items]}
  end
end

add_item/2 forgot to update total_cents. Nothing in the function is wrong on its own terms, and no guard, typespec, or pattern would object — but the invariant is checked on the way out:

# Cart.add_item(%Cart{}, %{sku: "A", cents: 500})
** (Bond.InvariantError) invariant violated around Cart.add_item/2
|   at: lib/cart.ex:6
|   label: :total_matches_items
|   assertion: subject.total_cents == Enum.sum(Enum.map(subject.items, & &1.cents))
|   binding: [subject: %Cart{items: [%{cents: 500, sku: "A"}], total_cents: 0}]

Checked in every implementation of a behaviour. Declare the contract once, on the callback, and every implementing module enforces it — without a line of contract code in any of them:

defmodule Paginator do
  use Bond.Behaviour

  @post never_over_limit: length(result) <= limit
  @callback fetch(page :: pos_integer(), limit :: pos_integer()) :: list()
end

defmodule LegacyPages do
  use Bond, behaviours: [Paginator]

  @impl true
  def fetch(page, _limit), do: Enum.map(1..50, &{page, &1})   # ignores limit
end
** (Bond.PostconditionError) postcondition (inherited from Paginator) failed in LegacyPages.fetch/2
|   at: lib/paginator.ex:4
|   label: :never_over_limit

The violation is attributed to the behaviour that declared it, and points at the line in that file. A promise made by an interface, kept by everything that implements it.

Checked against inputs you never thought of. The contracts you have already written are a specification, so they can serve as the oracle for property-based testing. You supply generators; Bond supplies the expected behaviour:

defmodule Roots do
  use Bond

  @pre non_negative: x >= 0.0
  @post never_negative: result >= 0.0
  @post shrinks_above_one: (x > 1.0) ~> (result < x)
  def sqrt(x), do: :math.sqrt(x)
end
# in test/roots_test.exs
use Bond.PropertyTest

contract_holds &Roots.sqrt/1, args: [StreamData.float(min: 0.0)]

That runs sqrt/1 against a stream of generated floats and fails if any precondition, postcondition, or check is violated, with StreamData shrinking to a minimal counterexample. Those two postconditions are the whole oracle — there is no separate model of "expected output" to write or keep in step, because the contract already said it. (~> is implication: shrinks_above_one asserts nothing unless x > 1.0.) See Testing Contracts for probe_contract/2, which reads the boundaries out of your @pre and aims generators at them, and invariants_hold/2, which throws random sequences of operations at a struct.

You choose what they cost

Contracts are checked at runtime, so they are not free — the Overhead guide publishes measured per-call figures. What makes that affordable is that the decision is yours, per environment and per contract kind:

# config/prod.exs
config :bond, preconditions: :purge, postconditions: :purge, invariants: :purge

Purged contracts are not compiled in at all — there is no check to skip, and the function runs exactly as if the contract had never been written. Your published documentation still shows it, because mix docs runs in :dev where contracts are enabled: the contract stays part of the module's stated interface even in builds that do not check it.

Between "on" and "purged" there is a third setting that compiles the check in but leaves it switched off, so a release can run with contracts inert and have them enabled from a remote console while a problem is being diagnosed. See Configuring Contracts.

Contracts are normally on in dev and test. What you keep in production is a separate decision — often nothing, often just the preconditions, which are the cheapest kind and the only one that tells you a caller is at fault. Either way, that is why it is worth writing the expensive, interesting ones.

Installation

Add bond to your dependencies in mix.exs:

def deps do
  [
    {:bond, "~> 1.14"}
  ]
end

Then run mix deps.get. Bond's only dependency is :telemetry; :stream_data is optional and needed solely for the property-testing macros. Bond starts no processes and adds nothing to your supervision tree — use Bond is compile-time machinery, and the runtime side is plain function calls.

Where to go from here

Bond does more than the examples above. The rest of the documentation is organised around the questions that tend to arrive in this order:

Summary

Types

Type to represent a compile-time quoted assertion expression, which must be a valid Elixir expression that, when unquoted, evaluates to a boolean/0 or as_boolean/1 value.

Type to represent a label for an assertion, which must be a compile-time atom or string.

Functions

use Bond enables @pre, @post, and check/1 annotations in the using module.

Override Kernel.@/1 to support @pre and @post annotations.

Check an assertion or a keyword list of assertions for validity.

Define a reusable, named contract that other functions apply with @apply_contract.

Register an invariant as a fully-qualified call, the qualified-call equivalent of @invariant. Accepts a bare expression or a keyword list of label: expression pairs; expressions reference the implicit subject binding exactly as in the @invariant form.

Register a postcondition as a fully-qualified call. See Bond.pre/1 and the :at_annotations option of use Bond for context; this is the qualified-call equivalent of @post.

Strengthen an inherited postcondition, the qualified-call equivalent of @post_strengthen (#16).

Register a precondition as a fully-qualified call, for modules that opt out of the @-prefixed syntax with use Bond, at_annotations: false.

Weaken an inherited precondition, the qualified-call equivalent of @pre_weaken (#16).

Types

Link to this type

assertion_expression()

View Source
@type assertion_expression() :: {atom(), Macro.metadata(), list()}

Type to represent a compile-time quoted assertion expression, which must be a valid Elixir expression that, when unquoted, evaluates to a boolean/0 or as_boolean/1 value.

@type assertion_label() :: String.t() | atom()

Type to represent a label for an assertion, which must be a compile-time atom or string.

Functions

Link to this macro

__using__(opts)

View Source (macro)

use Bond enables @pre, @post, and check/1 annotations in the using module.

When the module also inherits contracts (use Bond, behaviours: […]), @pre_weaken and @post_strengthen are additionally available to refine an inherited contract — weakening a precondition and strengthening a postcondition respectively, per Eiffel's behavioural-subtyping rules. See Bond.Behaviour.

Options

Each of the following options is one of true, false, or :purge. See the Configuring Contracts guide for what each value means. Options passed to use Bond override both the global :bond config and any :overrides entry that matches this module.

  • :preconditions — mode for this module's @pre annotations.
  • :postconditions — mode for this module's @post annotations.
  • :checks — mode for this module's check/1 calls.
  • :invariants — mode for this module's @invariant annotations.

Example: a hot-path module that wants contracts purged from its compiled output regardless of the global config.

defmodule MyApp.HotPath do
  use Bond, preconditions: :purge, postconditions: :purge, invariants: :purge
end

Purge from the top down: the contract-checking chain requires that a :purged kind has every kind above it :purged too, so preconditions: :purge on its own is a compile error.

:at_annotations

Controls Bond's @-prefixed annotation syntax — @pre, @post, and @invariant. By default (true) Bond overrides Kernel.@/1 in the using module so those forms are recognised. Overriding @ is lexically scoped to this module, so it is invisible to the rest of your project — but it cannot coexist within a single module with another library that also overrides @ (for example Norm's @contract).

Pass at_annotations: false to leave Kernel.@/1 untouched in this module. Bond's compiler hooks are still installed, but the @pre/@post/@invariant forms are not available; instead, write contracts as fully-qualified calls — Bond.pre/1, Bond.post/1, and Bond.invariant/1. check/1 remains available unqualified.

defmodule MyApp.Validated do
  use Norm
  use Bond, at_annotations: false

  @contract add(integer(), integer()) :: integer()
  Bond.pre x >= 0 and y >= 0
  Bond.post result >= 0
  def add(x, y), do: x + y
end

Contract sections are omitted from generated docs

With the @ override off, your @doc goes straight to Kernel and Bond never sees it, so it cannot append the #### Preconditions / #### Postconditions sections it normally adds. Bond leaves documentation entirely alone in this mode rather than emit a doc that would replace your own prose. Contracts are enforced exactly as usual; only their appearance in generated documentation is affected.

Bare macros are always fully-qualified

The pre/post/invariant macros are never imported, even with the default at_annotations: true. This keeps them from colliding with common function names (notably post) in modules that only ever use the @ forms. They are reachable only as Bond.pre, Bond.post, and Bond.invariant.

Override Kernel.@/1 to support @pre and @post annotations.

See the Writing Contracts guide for the syntax of @pre and @post annotations.

Link to this macro

check(assertion_or_list_of_assertions)

View Source (macro)
@spec check(assertion_expression()) :: as_boolean(any())
@spec check(Keyword.t(assertion_expression())) :: [as_boolean(any())]

Check an assertion or a keyword list of assertions for validity.

Returns the result(s) of the assertion(s) if satisfied, or raises a Bond.CheckError exception if any assertions are not satisfied.

Examples

iex> check 1 == 1.0
true
iex> check tautology: 1 == 1
[true]
iex> check "1 is 1": 1 == 1, "2 is 2": 2 == 2
[true, true]

Conditional compilation

check honours the :bond, :checks configuration:

  • :purgecheck calls in modules that use Bond expand to :ok at compile time and the wrapped expression is not evaluated at all. Don't rely on side effects in checks.
  • true (default) — check calls expand to a runtime-guarded evaluation; the guard reads the runtime mode for :checks on every call and evaluates unless it is false.
  • false — same shape as true, but the runtime default flips to false (off unless re-enabled).

Compile-time defaults come from config :bond, checks: … (and use Bond opts). To toggle at runtime, use Bond.Config.enable(:checks) / Bond.Config.disable(:checks)Application.put_env/3 after the first contracted call is not picked up. See Bond.Config.

Link to this macro

defcontract(head)

View Source (macro)
Link to this macro

defcontract(head, arg2)

View Source (macro)

Define a reusable, named contract that other functions apply with @apply_contract.

A named contract bundles @pre/@post under a {name, arity} so the same agreement can be shared across functions instead of being restated on each one. The head's parameter list supplies the contract's canonical argument names and their order; a function that applies the contract has its parameters rebound to those names positionally (so it may name them however it likes), exactly as an implementation inherits a Bond.Behaviour callback's contract.

defmodule Money do
  use Bond

  defcontract withdrawal(account, amount) do
    @pre sufficient: amount <= account.balance
    @post non_negative: result.balance >= 0
  end
end

defmodule Account do
  use Bond

  @apply_contract {Money, :withdrawal}
  def withdraw(acct, amt), do: %{acct | balance: acct.balance - amt}
end

Contracts are keyed by {name, arity}, so name(x) and name(x, y) are distinct overloads; the applying function's arity selects which one binds. A contract body may contain only @pre/@post, and each expression may reference only the contract's declared arguments (plus result in a @post).

Zero-argument (result-only) contracts

A contract whose @post constrains only the return value — never any argument name — can be shared across functions of any arity by declaring it with an explicit empty parameter list:

defcontract gate_result() do
  @post {:ok, :cleared} <~ result or
          ({:error, :validation_failed, errs} when is_list(errs)) <~ result
end

@apply_contract :gate_result
def can_encode_previews?(game_film), do: 

@apply_contract :gate_result
def can_encode?(game_film, exchange_file), do: 

The empty () is explicit and required — defcontract gate_result do … end (no parens) raises a CompileError. The wrapper and super call still forward the applying function's actual arguments; only the result binding in the lifted postcondition defp is constrained by the contract. Preconditions may not appear in a zero-argument contract (there are no argument names to reference).

Link to this macro

invariant(expression_or_kw_list)

View Source (macro)

Register an invariant as a fully-qualified call, the qualified-call equivalent of @invariant. Accepts a bare expression or a keyword list of label: expression pairs; expressions reference the implicit subject binding exactly as in the @invariant form.

Bond.invariant subject.size >= 0
Link to this macro

post(expression)

View Source (macro)

Register a postcondition as a fully-qualified call. See Bond.pre/1 and the :at_annotations option of use Bond for context; this is the qualified-call equivalent of @post.

Link to this macro

post_strengthen(expression)

View Source (macro)

Strengthen an inherited postcondition, the qualified-call equivalent of @post_strengthen (#16).

See Bond.pre_weaken/1 and the :at_annotations option of use Bond. The effective postcondition becomes inherited and post_strengthen.

Link to this macro

pre(expression)

View Source (macro)

Register a precondition as a fully-qualified call, for modules that opt out of the @-prefixed syntax with use Bond, at_annotations: false.

Bond.pre/1 is the qualified-call equivalent of @pre; the registered precondition is enforced identically. It accepts either a bare assertion expression or a keyword list of label: assertion pairs. Labels are atoms — quote for spaces or punctuation:

Bond.pre x > 0
Bond.pre positive: x > 0, bounded: x < 100
Bond.pre "x must be positive": x > 0
Link to this macro

pre_weaken(expression)

View Source (macro)

Weaken an inherited precondition, the qualified-call equivalent of @pre_weaken (#16).

For modules that opt out of the @-prefixed syntax with use Bond, at_annotations: false. The effective precondition becomes inherited or pre_weaken; see Bond.Behaviour for the Eiffel-style refinement rules. Accepts a bare assertion or a keyword list of label: assertion pairs, exactly like Bond.pre/1.