Declare @pre/@post contracts on a behaviour's @callbacks and have them enforced on every implementing module.

This is where Design by Contract meets the Liskov Substitution Principle: a behaviour is a promise about a family of implementations, and a contract is the formal content of that promise. A module that use Bond.Behaviour attaches contracts to its callbacks; a module that use Bond, behaviours: [TheBehaviour] inherits and enforces those contracts on its own clauses.

defmodule Ledger do
  use Bond.Behaviour

  @pre positive_amount: amount > 0
  @post non_negative: result >= 0
  @callback withdraw(balance :: non_neg_integer, amount :: pos_integer) :: non_neg_integer
end

defmodule BankAccount do
  use Bond, behaviours: [Ledger]

  @impl true
  def withdraw(balance, amount) when amount <= balance, do: balance - amount
end

A @pre/@post precedes the @callback it attaches to, exactly as a contract precedes the def it attaches to in use Bond. The contract expressions reference the callback's argument names (balance, amount above); those names become canonical, and an implementation's parameters are rebound to them positionally — so the impl is free to name its parameters differently.

Inheriting verbatim

By default an implementation inherits its callbacks' contracts verbatim. Attaching a plain @pre/@post to an impl function whose {name, arity} matches an inherited contract is a compile error: a plain impl-level precondition would strengthen the inherited one, which breaks Liskov substitutability. For an implementation-specific assertion that is independent of the contract, use Bond.check/1 in the body.

Refining inherited contracts (@pre_weaken / @post_strengthen)

An implementation may deliberately refine what it inherits, following Eiffel's behavioural-subtyping rules. Two distinct annotations make the (counterintuitive) variance explicit:

• @pre_weaken — weakens the precondition. The effective precondition is inherited or pre_weaken: the impl accepts everything the abstraction promised, and more. (Preconditions may only weaken down a hierarchy — contravariance.)
• @post_strengthen — strengthens the postcondition. The effective postcondition is inherited and post_strengthen: callers get at least the abstract guarantee, and more. (Postconditions may only strengthen — covariance.)

Refinement expressions reference the callback's argument names — the same vocabulary as the inherited contract they amend — not the implementation's own parameter names. The implementation may still name its parameters however it likes; the refinement just binds by the callback's names. (Protocol refinement via Bond.Protocol.Impl follows the identical rule.)

defmodule SavingsAccount do
  use Bond, behaviours: [Ledger]   # callback: withdraw(balance, amount)

  # 'amount' is Ledger's callback argument name, even though this clause names it 'amt'.
  @impl true
  @pre_weaken small_withdrawal: amount == 0     # effective pre  = Ledger's OR this
  @post_strengthen audited: log_exists?(result) # effective post = Ledger's AND this
  def withdraw(bal, amt), do: ...
end

A refinement only applies to a function that inherits a contract. @pre_weaken requires an inherited precondition to weaken (you may not introduce one — that would strengthen); @post_strengthen may add a postcondition where the callback declared none. old/1 is not available in @post_strengthen (it remains available in the inherited @post).

Reflection

use Bond.Behaviour generates a __bond_contracts__/0 function on the behaviour module that returns its callback contracts keyed by {name, arity}. It is an internal reflection hook read by use Bond, behaviours: […] at the implementer's compile time; you should not call it directly.