View Source Bond.Protocol.Impl (Bond v1.7.0)

Opt-in contract refinement for a defimpl block.

use Bond.Protocol.Impl inside a defimpl lets that implementation refine the contracts it inherits from the protocol, following Eiffel's behavioural-subtyping rules:

• @pre_weaken weakens the inherited precondition — effective pre = inherited OR pre_weaken. The implementation accepts everything the abstraction promised, and more (contravariance).
• @post_strengthen strengthens the inherited postcondition — effective post = inherited AND post_strengthen. Callers get at least the abstract guarantee, and more (covariance).

Refinement expressions reference the canonical argument names declared in the protocol's own def, not the implementation parameter names (which are often patterns rather than simple variables).

Usage

defprotocol Account do
  use Bond.Protocol

  @pre positive_amount: amount > 0
  @post non_negative: result >= 0
  def withdraw(data, amount)
end

defimpl Account, for: SavingsAccount do
  use Bond.Protocol.Impl

  # Accept zero-amount withdrawals too (no-op); canonical name 'amount' from protocol
  @pre_weaken zero_ok: amount == 0
  # Also guarantee the balance changed (or stayed the same on zero withdrawal)
  @post_strengthen unchanged_on_zero: amount == 0 or result < data.balance
  def withdraw(acc, 0), do: acc.balance
  def withdraw(acc, amount), do: acc.balance - amount
end

A @pre_weaken is only valid when the protocol declares a precondition for that function; @post_strengthen may add a postcondition even if the protocol declared none. old/1 is not supported in either annotation (protocol contract v1 restriction).

Implementations that do not use Bond.Protocol.Impl are completely unaffected.