jonnifyelixir
F5 · Pragmatic Programming / F5.04 · contracts

F5 · the engine · module 4

Design by contract

The contract triad Three deep dives

The walking skeleton runs, but its commands trust whatever they are handed. Design by contract makes that trust explicit. Every command carries three terms: a precondition the caller must satisfy to call it, a postcondition the command guarantees on success, and an invariant that is always true of the state, before and after. For enroll: the ids must be valid and the learner not already on the course; on success a fresh %Enrollment{} with progress: 0 is returned and stored; and progress never leaves 0..100. Elixir has no contract keywords, so these are written as guards, with chains, and tagged tuples — and they fail fast, at the boundary, before anything can be corrupted.

A contract wraps a command on three sides. Select a term to see what it says for enroll and who is responsible for it.

Where a violation is caught

A CALL WITH progress: 250 boundary gateprecondition stops it here commandnever runs storeuntouched

caught at the gate · store intact
A precondition fails fast: the error lands at its cause.

The contract triad

Read it left to right: the precondition is checked before the command runs, the postcondition holds when it returns, and the invariant constrains the state the whole time. The precondition protects the command from bad input; the postcondition lets the caller trust the result without re-checking; the invariant protects the entity from ever reaching an illegal shape. Select a term.

The enroll contract · select a term

PRECONDITION valid ids, not enrolled COMMAND enroll(user_id, course_id) POSTCONDITION {:ok, %Enrollment{}} INVARIANT · ALWAYS TRUE OF THE STATE 0 <= progress <= 100 · user_id is always a USR

term: Precondition

for enroll: valid ids, not already enrolled

A contract turns assumptions into checks. Once the three terms are written down, “is this safe to call” has an answer in the code, not in your head.

Three deep dives

In order: the three terms of a contract and who owns each; how to express them in idiomatic Elixir; and why a contract must fail fast at the boundary rather than late and quietly.

F5.04.1
Preconditions, postconditions & invariants
Three terms, three owners: the caller meets the precondition, the function guarantees the postcondition, every operation preserves the invariant.
F5.04.2
Assertions in Elixir
Guards for shape, a with chain to compose checks, tagged tuples for expected failures, and raise for broken invariants.
F5.04.3
Failing fast
Stop on the first violation, at the boundary, before any state changes — an error close to its cause beats corruption far from it.

F5.03 · the slice runs

Enroll travels every layer, but it trusts its inputs and promises nothing in particular.

F5.04 · make the command honest

State its precondition, guarantee its postcondition, preserve the invariant — and fail fast when broken.

Start with the three conditions, then assertions in Elixir, then failing fast. The next module, F5.05 — Commands, queries & events, separates writes from reads and models each change as an event. For the runtime path the contract guards, see the design brief: the command & event flow.

References

Contracts on functions, and the Elixir idioms that express them.

Sources

Related in this course