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.

Write remote calls fully qualified

A contract expression is expanded in each implementing module, so it resolves in that module's alias scope — not this one. An alias here does not travel with the contract; a short name that resolves at the declaration site fails in every implementation that does not happen to alias the same module. Spell remote calls and struct literals out in full. See the Contract Inheritance guide.

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.