Preconditions, postconditions & invariants

A contract is an agreement between a caller and a function, and like any contract it assigns obligations. The precondition is the caller’s obligation — what must hold before the call. The postcondition is the function’s obligation — what it guarantees on return, given the precondition held. The invariant is a shared obligation on the data itself — what every operation must leave true. The value of naming them is precise blame: when something breaks, the term that broke says exactly whose fault it is, and that tells you whether you have a bad request or a bug.

Three terms, three owners. Select one to see who must guarantee it and what that buys the other side.

Who owns each term In code Invariants that always hold

Who owns each term

The asymmetry is the point. Because the caller owns the precondition, the function may assume it and need not defend against what it forbids. Because the function owns the postcondition, the caller may trust the result blindly. The invariant binds both: no operation may leave the entity in a shape its type forbids. Select a term to see its owner.

The three terms · select one

term: Precondition

owner: the caller

Name the owner and you name the fault. A broken precondition is the caller’s; a broken postcondition is the function’s; a broken invariant is a defect in the type itself.

In code

Write the contract down, even before you enforce it. As documentation, the three terms tell the next reader the rules; in the body they map onto a guard or check for the precondition, the returned shape for the postcondition, and a constraint every operation respects for the invariant.

# @precondition  user_id is a USR, course_id is a CRS, learner not already enrolled  (caller)
# @postcondition {:ok, %Enrollment{progress: 0}}, stored                              (function)
# @invariant     0 <= progress <= 100                                                  (always)
def enroll(user_id, course_id) do
  with :ok <- check_precondition(user_id, course_id) do
    enrollment = %Enrollment{id: Portal.ID.new("ENR"), user_id: user_id, course_id: course_id}
    Portal.Store.put(enrollment)
    {:ok, enrollment}            # postcondition holds: progress defaults to 0
  end
end

an agreement

Caller and function each owe the other something; the invariant binds the data they share.

precise blame

The term that breaks tells you whether it is a bad request or a bug.

Next: assertions in Elixir — the idioms that turn these three terms into running checks.

Invariants that always hold

The progress range is a one-field invariant; most invariants relate several fields. Bertrand Meyer’s Applying Design by Contract calls such a constraint a class invariant: a property the data keeps at all times, asserted at every point an instance is observable from outside. A Portal.Learning.Roster record carries two fields — the lessons enrolled in and the lessons completed — bound by one rule: $\textit{completed} \subseteq \textit{enrolled}$. A completed lesson that was never enrolled is not a bad request; it is an impossible state, so the type must never hold it.

Meyer’s lever is that the invariant need be checked in only one place. If every instance is built through a single checked constructor, and the fields are immutable thereafter, then proving the rule once at construction proves it for the whole lifetime. @enforce_keys forbids a struct literal that omits a required field, and Portal.Learning.Roster.new/1 is the one door through which a value is admitted — it raises on a violation rather than returning a tagged error, because a broken invariant is a defect in the caller’s logic, not an expected outcome.

The one rule a Roster keeps: completed ⊆ enrolled

defmodule Portal.Learning.Roster do
  # @invariant  completed is a subset of enrolled  (held at all times)
  @enforce_keys [:learner_id, :enrolled, :completed]
  defstruct [:learner_id, :enrolled, :completed]

  # the one door: the only sanctioned way to build a Roster
  def new(%{learner_id: id, enrolled: enrolled, completed: completed}) do
    enrolled = MapSet.new(enrolled)
    completed = MapSet.new(completed)

    unless MapSet.subset?(completed, enrolled) do
      raise ArgumentError, "completed must be a subset of enrolled"
    end

    %Portal.Learning.Roster{learner_id: id, enrolled: enrolled, completed: completed}
  end
end

# the invariant holds — the value is admitted
Portal.Learning.Roster.new(%{learner_id: "USR_7f", enrolled: ["L1", "L2", "L3"], completed: ["L1"]})
# => %Portal.Learning.Roster{learner_id: "USR_7f", enrolled: #MapSet<["L1", "L2", "L3"]>, completed: #MapSet<["L1"]>}

# a completed lesson that was never enrolled — an impossible state, rejected at the door
Portal.Learning.Roster.new(%{learner_id: "USR_7f", enrolled: ["L1"], completed: ["L1", "L9"]})
# => ** (ArgumentError) completed must be a subset of enrolled

a class invariant

One rule the data keeps for its whole lifetime, not a check a single function performs.

checked once, at the door

@enforce_keys plus a raising new/1 make construction the only place state is built.

An invariant proven at the single point a value is constructed, on immutable fields, is an invariant that cannot later be false.

References

Primary sources for this lesson, and where it connects in the course.

Sources

Bertrand Meyer — Applying Design by Contract — preconditions, postconditions, invariants.
Eiffel — Design by Contract and assertions — the contract metaphor, in depth.
Elixir — Patterns and guards — guards as executable preconditions.