View Source Bond.InvariantError exception (Bond v1.9.0)
Exception raised when an invariant is violated.
Covers all three invariant flavours, distinguished by the :kind field:
- a struct
@invariant(:kind:invariant) — checked when a public function in the struct's defining module receives or returns a value of the struct (:functionis that function); - a
Bond.Server@state_invariant(:kind:state_invariant) — checked after every state-transition callback returns a new state (:functionis that callback); - a
Bond.Server@transition_invariant(:kind:transition_invariant) — checked across every transition callback, relatingold_statetonew_state(:functionis that callback).
Summary
Types
The Bond.InvariantError exception type.
Types
@type t() :: %Bond.InvariantError{ __exception__: term(), binding: keyword(), expression: Bond.assertion_expression(), file: Path.t(), function: {String.t(), non_neg_integer()}, impl: module() | nil, kind: atom(), label: Bond.assertion_label(), line: integer(), module: module(), quantifier: map() | nil, source_behaviour: module() | nil, source_contract: {module(), atom()} | nil, source_protocol: module() | nil }
The Bond.InvariantError exception type.
:kind is the assertion kind (:precondition, :postcondition, :invariant,
:state_invariant, :transition_invariant, or :check). For Bond.InvariantError it
distinguishes a struct @invariant from a Bond.Server @state_invariant /
@transition_invariant; for the others it is redundant with the struct type.
:source_behaviour is the behaviour module an inherited contract came from (see
Bond.Behaviour), or nil for a contract declared directly on the function.
:source_contract is the {module, name} of an applied named contract the failing
assertion came from (see defcontract/@apply_contract), or nil otherwise.
:source_protocol is the protocol module a contract was declared on (see Bond.Protocol),
or nil; when set, :impl is the implementation module the failing call resolved to (or
nil if none could be resolved).
:quantifier carries element-level failure detail when the assertion used forall/exists
(see Bond.Predicates), or nil otherwise.