Module 6: Stateful Property Testing

6. `@invariant`: what must always hold

Next →

Description

Your machine already has state, two operations and the flow of bookings between them. And yet, so far it doesn't check anything: it generates sequences, executes them, and only fails if an operation blows up with an unexpected exception. It is missing the heart —the part that turns "executing operations" into "catching bugs." That heart is the @invariant: a rule Hypothesis checks after each operation, and that must hold regardless of which sequence has been executed up to that point.

An invariant is the stateful version of a property. In modules 1 to 5, a property asserted something about the output of one call. An invariant asserts something about the state of the system at any moment of its history: "there are never two overlapping confirmed bookings in the same room," "a cancelled booking never counts as occupied," "the number of confirmed ones matches the bookings made minus the cancelled." Note the shape: it doesn't talk about an operation ("after cancelling, X happens"), it talks about the whole system, always. Hypothesis verifies it after the first book, after the second, after the cancel, after each step —so that if some operation leaves the system in an impossible state, it is discovered the instant it happens. By the end of this lesson you are going to have the complete machine: state, rules, bundle and invariants, running green against the correct Calendar. It is the machine we will put in front of a bug in lesson 7.

Connection with the module: this lesson closes the construction. It adds to the machine of lesson 5 the piece that was missing —the invariants— and with that the machine is whole. It also presents @initialize, to start the machine in a given state. Lesson 7 adds nothing structural: it takes this same complete machine and runs it against a buggy book, to see an invariant jump and read the falsifying sequence. So this is the last "building" lesson; the next is the "catching" one. We continue with Reservo's correct Calendar, verifying the three invariants over it.

An analogy: the chess rules that are never broken

Think of the rules of a chessboard, but not the ones of how each piece moves —those would be the rules of the operations—, rather the ones that describe states that can never occur, no matter what happens in the game. "There are never two pieces on the same square." "Each side has exactly one king." "A pawn is never on the first or last rank (it promotes on arriving)." These are not rules of a move; they are truths about the board at every moment, after any sequence of plays. If at some instant of the game you find two pieces on the same square, you know something broke —no matter which plays led there.

An @invariant is one of those truths about the board. It doesn't say "after moving the knight, such a thing happens"; it says "in any configuration of the board the game can produce, there are never two pieces on the same square." And the way to watch it is to check the board after each play: if after some move the impossible configuration appears, there is the bug, and the play that just happened is suspicious. That is exactly what Hypothesis does with your invariants: after each book and each cancel, it looks at the state of the calendar and verifies that none of the sacred truths was violated. The invariant is the definition of "impossible state"; the machine is the referee that checks the board play by play.

Worked example: the complete machine with three invariants

We take the machine of lesson 5 (with Bundle) and add three invariants. One of them —the count one— needs the machine to carry a model: a counter self.confirmed that says how many confirmed bookings there should be according to the successful operations. Comparing that model with reality is one of the most powerful techniques of stateful testing.

# test_machine_full.py -- book + cancel + Bundle + invariants, against the CORRECT code
from datetime import datetime, timedelta

from hypothesis import strategies as st
from hypothesis.stateful import (
    RuleBasedStateMachine, rule, invariant, Bundle, consumes, multiple,
)

from reservo import Calendar, book, cancel, overlaps, RoomUnavailable

BASE = datetime(2026, 3, 10, 0, 0)
ROOM = "r-focus"


class CalendarMachine(RuleBasedStateMachine):
    bookings = Bundle("bookings")

    def __init__(self):
        super().__init__()
        self.calendar = Calendar()
        self.next_id = 0
        self.confirmed = 0   # model: how many confirmed we think there are

    @rule(target=bookings,
          start_hour=st.integers(min_value=0, max_value=10),
          length=st.integers(min_value=1, max_value=4))
    def book_room(self, start_hour, length):
        start = BASE + timedelta(hours=start_hour)
        end = start + timedelta(hours=length)
        booking_id = f"bk-{self.next_id}"
        self.next_id += 1
        try:
            book(self.calendar, booking_id, ROOM, "m-1", start, end, price_cents=1000)
        except RoomUnavailable:
            return multiple()
        self.confirmed += 1
        return booking_id

    @rule(booking_id=consumes(bookings),
          hours_before=st.integers(min_value=0, max_value=100))
    def cancel_booking(self, booking_id, hours_before):
        booking = self.calendar.get(booking_id)
        now = booking.start - timedelta(hours=hours_before)
        cancel(self.calendar, booking_id, now)
        self.confirmed -= 1

    # --- invariants: must hold after ANY sequence of operations ---

    @invariant()
    def no_two_confirmed_overlap(self):
        confirmed = self.calendar.confirmed_for_room(ROOM)
        for i in range(len(confirmed)):
            for j in range(i + 1, len(confirmed)):
                a, b = confirmed[i], confirmed[j]
                assert not overlaps(a.start, a.end, b.start, b.end), (
                    f"two confirmed overlapping in the same room: {a.id} and {b.id}")

    @invariant()
    def cancelled_never_counts_as_confirmed(self):
        confirmed_ids = {b.id for b in self.calendar.confirmed_for_room(ROOM)}
        for b in self.calendar.all_bookings():
            if b.status == "cancelled":
                assert b.id not in confirmed_ids, (
                    f"a cancelled booking appears as confirmed: {b.id}")

    @invariant()
    def count_matches_model(self):
        real = len(self.calendar.confirmed_for_room(ROOM))
        assert real == self.confirmed, (
            f"count out of sync: real={real}, model={self.confirmed}")


TestCalendar = CalendarMachine.TestCase

Let's take apart the three invariants, because each illustrates a different type of state truth:

  • no_two_confirmed_overlap — the "impossible state" invariant. It goes through all the pairs of confirmed bookings of the room and asserts that none overlaps with another. It is the sacred rule of the calendar: two confirmed bookings can never step on each other in the same room. It doesn't mention any operation; it describes a forbidden configuration of the board. This is the invariant lesson 7 will see jump.
  • cancelled_never_counts_as_confirmed — the "consistency between views" invariant. It asserts that if a booking is marked as cancelled, it doesn't appear in the list of confirmed ones. With the correct Calendar it is true by construction (confirmed_for_room filters by status == "confirmed"), but stating it as an invariant protects it: if someone broke that filter, or if cancel left a booking in a hybrid state, this invariant would catch it.
  • count_matches_model — the model invariant. Here the machine carries its own count (self.confirmed): it raises it when a book succeeds, lowers it when a cancel occurs. The invariant compares that count with reality (len(confirmed_for_room)). It is the most general form of invariant: a simplified model of the system running in parallel, and the assertion that the real system matches it. If book or cancel altered the count unexpectedly, reality would come apart from the model and the invariant would jump.

What to expect. You save and run python3 -m pytest test_machine_full.py. Green: Hypothesis generates many sequences that mix book and cancel, and after each operation of each sequence it checks the three invariants. None is violated, because the Calendar is correct:

$ python3 -m pytest test_machine_full.py
test_machine_full.py .                                                   [100%]

============================== 1 passed in 0.68s ===============================

With --hypothesis-show-statistics you would see the detail: a hundred sequences generated, plus a handful of "invalid" cases. Those invalids are interesting: they occur when Hypothesis wants to execute cancel_booking but the bundle is empty (there are no bookings to cancel), so it discards that attempt and tries another sequence. It is the bundle doing its job —it never passes cancel a nonexistent id—, visible in the statistics as cases that never got to test anything.

Note what just happened: the machine ran hundreds of operations spread across a hundred different histories, and after each one it verified three truths of the calendar. That "after each one" is what makes the technique so fine: it doesn't wait until the end of the sequence to check; it checks step by step, so as soon as an operation leaves the system wrong, it is known immediately which one it was.

@initialize: starting the machine in a given state

Sometimes you don't want the machine to start from a totally empty state. Maybe your invariant only makes sense if there is already something in the system, or you want all the sequences to start with a base booking placed. For that there is @initialize: a method Hypothesis executes exactly once, at the beginning of each sequence, before any @rule.

@initialize(target=bookings)
def seed_with_one_booking(self):
    # ALWAYS starts with a base booking from 00:00 to 01:00 already confirmed
    book(self.calendar, "bk-seed", ROOM, "m-1", BASE, BASE + timedelta(hours=1), price_cents=1000)
    self.confirmed += 1
    return "bk-seed"

What to expect. A machine with this @initialize runs green just like the previous one, but now all the sequences start with bk-seed already confirmed:

$ python3 -m pytest test_machine_initialize.py -v
test_machine_initialize.py::TestCalendar::runTest PASSED                  [100%]

============================== 1 passed in 0.76s ===============================

@initialize resembles a @rule, but with two key differences. First, it runs a single time and at the beginning: it is not an operation Hypothesis interleaves in the sequence, but the stage setup before the performance starts. Second, it can have target (like here, where it deposits bk-seed in the bundle so the rules can cancel it) and can receive strategies as arguments (to start in a random but controlled state). The difference with putting the initial state in __init__ is subtle but important: what goes in __init__ is fixed and always the same; what goes in @initialize can deposit in bundles and use strategies, integrating with Hypothesis's machinery. Practical rule: mute and fixed state (the empty Calendar, the counter at zero) in __init__; seeding that interacts with bundles or strategies, in @initialize.

What makes an invariant good

Not just any assertion serves as an invariant. The machine's three illustrate the qualities you look for, and it is worth naming them because finding good invariants is —like finding good properties in module 4— the part that truly costs.

A good invariant talks about the state, not about an operation. "Never two overlapping confirmed" is an invariant; "after book, the booking is confirmed" is not —that is a postcondition of an operation, and it goes inside the rule or in a separate test. The test: an invariant must be checkable at any moment, without knowing which operation just ran. If your assertion needs to know "I just did X," it is not a state invariant.

A good invariant prohibits impossible states or asserts global consistencies. The two flavors you saw: prohibit the impossible (two overlapping, negative balance, two pieces on one square) or assert that two views of the system agree (the real count matches the model; the cancelled one doesn't appear as confirmed). Both capture the health of the system as a whole, not the result of a step.

A good set of invariants covers itself. Just as in module 4 a function needed several properties, a stateful system needs several invariants, because each catches a different class of bug. You will see in lesson 7 that the overlap invariant catches the all/any bug, but the count one doesn't —both raise the counter the same—; and in lesson 8, that the count one catches a cancel that forgets to mark, but the overlap one doesn't. No single one suffices. The same underlying lesson from module 4, now about invariants: don't look for the perfect invariant; gather several modest ones that cover the gaps between each other.

The model invariant (count_matches_model) deserves a separate paragraph because it is the most powerful and the most general. The idea: you write a simplified model of the system —here, a simple integer that counts confirmed— that is so simple it is obviously correct, you update it in parallel with each operation, and you assert that the real system matches it. It is the oracle pattern of module 4, but for state: the model is the oracle, and the machine verifies that the real implementation (complicated, with its calendar and its overlaps) never comes apart from the simple reference. Models can be richer than an integer —a dictionary of occupied hours, a set of ids— but the rule is the same: keep the model so simple that you can't get it wrong writing it, because a model with the same bug as the system proves nothing.

Common mistakes

Writing an operation postcondition disguised as an invariant. What happens: someone writes an @invariant that actually asserts something about the last operation ("the just-created booking is confirmed"), and it fails or makes no sense when the last operation was a cancel. Why it happens: "what is true after this operation" gets confused with "what is always true." How to detect it: if your invariant needs to know which the last operation was, or fails depending on which rule ran just before, it is not a state invariant. How to fix it: an invariant must hold after any operation. What you want to assert about a concrete operation ("after book, it is confirmed") goes as an assertion inside that rule, not as an @invariant.

A model that gets out of sync by not being updated on all the paths. What happens: someone carries a self.confirmed but forgets to decrement it on some path (or increments it even when book was rejected), and the count invariant jumps with a failure that is not the system's, but the model's. Why it happens: keeping the model in sync demands discipline on every branch. How to detect it: if the count invariant fails but on inspecting the calendar everything looks fine, suspect that the model lies, not the system. How to fix it: update the model exactly when the system changes, and on all the paths —increment only after a successful book (after the try, not in the except), decrement on each cancel. The model is a commitment: if you carry it badly, it produces false failures.

Checking the invariants only at the end instead of after each step. What happens: someone, misunderstanding the tool, puts the assertions at the end of a rule or in a teardown, instead of using @invariant, and loses the ability to know which operation broke the state. Why it happens: they don't take advantage of @invariant running after each step. How to detect it: if when something fails you don't know which operation caused it, maybe you aren't checking step by step. How to fix it: use @invariant for the state truths; Hypothesis verifies them after each operation, so the failure appears at the exact instant the state breaks, and the reproducer shows you the sequence up to that point. Checking only at the end tells you that something broke, but not when.

Exercises

Exercise 1

Reproduce test_machine_full.py with its three invariants and confirm it green with --hypothesis-show-statistics. In the statistics, look for the "invalid" cases. Explain why they appear and why they are not a problem.

View solution

The machine passes green. In the statistics you will see something like "100 passing, 0 failing, and N invalid test cases," with N a handful (in one run 23 came out).

The invalid cases appear when Hypothesis tries to assemble a sequence that includes cancel_booking at a moment when the bundle is empty —there is no live booking to cancel. Since cancel_booking consumes from the bundle (consumes(bookings)) and the bundle has nothing to offer, Hypothesis can't complete that step, so it discards the attempt and counts it as "invalid." It is not a failure or a problem: it is the bundle protecting you from calling cancel without a booking. Simply, those sequences didn't get to test anything useful and are discarded.

That they appear is a sign that the mechanism works: without the bundle (as in lesson 4), you would have had to write if not self.booked_ids: return to handle that case by hand; with the bundle, Hypothesis handles it by marking the attempt as invalid and continuing. A high number of invalids could suggest that the machine generates many useless sequences (and sometimes it is adjusted with weights or preconditions), but a handful is completely normal and healthy.

Exercise 2

Classify each assertion as "valid state invariant" or "operation postcondition (not an invariant)": (a) "the account balance is never negative"; (b) "after a deposit of 100, the balance went up exactly 100"; (c) "the number of pending tasks plus completed ones equals the total added"; (d) "after completing a task, it stops being pending."

View solution
  • (a) "the balance is never negative" — valid state invariant. It talks about the system at any moment, without referring to an operation. It can be checked after any deposit or withdrawal. It is of the "prohibits an impossible state" type.
  • (b) "after a deposit of 100, the balance went up 100" — postcondition, not an invariant. It needs to know the last operation was a deposit of 100. It can't be checked after a withdrawal. It goes as an assertion inside the deposit rule, not as an @invariant.
  • (c) "pending + completed = total added" — valid state invariant. It is a global consistency that holds at every moment, of the "model" type: it relates three quantities of the state without referring to an operation. It is checked after any step.
  • (d) "after completing a task, it stops being pending" — postcondition, not an invariant. It talks about the effect of a concrete operation (complete_task). It makes no sense to check it after an add_task. It goes inside the complete_task rule.

The mechanical test to distinguish them: can I check this assertion at any moment, without knowing which operation just ran? If yes (a, c), it is an invariant. If I need to know "I just did X" (b, d), it is a postcondition and goes inside the corresponding rule.

Exercise 3

The invariant count_matches_model compares reality with a model (self.confirmed). Explain why the model is a simple integer and not, for example, a complete copy of the calendar. What would be gained and what would be lost with a richer model?

View solution

The model is a simple integer because a model invariant is worth its simplicity: it has to be so obvious that it is impossible for it to have the same bug as the real system. A counter that does +1 on booking and -1 on cancelling is trivially correct; nobody gets it wrong writing it. If the model were a complete copy of the calendar —with its own overlap and state logic—, it would run the risk of having the same bug as the system it tests, and then "the model and reality match" would prove nothing (both would be wrong the same). It is the same danger as the oracle of module 4: an oracle that shares the bug is useless.

What would be gained with a richer model: it would catch more bugs. An integer only verifies how many confirmed there are; it doesn't verify which or where. A model that were, say, a set of the occupied intervals would catch bugs the count doesn't see —for example, a cancel that frees the wrong slot would leave the count fine but the set of intervals wrong. With more detail in the model, more finesse in the detection.

What would be lost: confidence and simplicity. The richer the model, the more logic it has, the easier it is to get it wrong, and the more it resembles the real system (with which the risk of sharing bugs grows). There is a balance: the model must be rich enough to catch the bugs that matter to you, but simple enough to be obviously correct. In practice you start simple (a counter) and enrich it only when a known bug demands it. That is why here the count is accompanied by the overlap invariant: between the two —one simple of quantity, another structural— they cover more than either alone, without needing a heavy model.

Summary and next step

In this lesson you gave the machine its heart: the @invariant, the state truths Hypothesis checks after each operation. You understood that an invariant is the stateful version of a property —it asserts something about the system at any moment of its history, not the effect of an operation—, and you wrote three: the "impossible state" one (no_two_confirmed_overlap), the "consistency between views" one (cancelled_never_counts_as_confirmed) and the model one (count_matches_model), where a simple counter runs in parallel as an oracle of the real system. The complete machine —state, rules, bundle, invariants— ran green against the correct Calendar.

You saw @initialize to start the machine in a seeded state (once, at the beginning, with access to bundles and strategies), and the qualities of a good invariant: that it talk about the state and not an operation, that it prohibit impossible states or assert global consistencies, and that several cover each other —because, like the properties of module 4, no single one catches all the bugs. And you learned the discipline of the model: keeping it so simple that it is obviously correct, and updating it on all the paths so it doesn't lie.

Before moving on you should be able to: write an @invariant that talks about the state; distinguish an invariant from a postcondition; carry a simple model and assert that the system matches it; and explain why several invariants are needed.

You have the complete machine and it is green. Now comes the moment that gives meaning to the whole module: putting it in front of a bug. In lesson 7 we run this same machine against a book with the all/any error, we see the overlap invariant jump, and —most important— we read the minimal falsifying sequence Hypothesis reduces, reproduce it by pasting it as is, and understand how the machine shrinks not an input but a whole sequence. Let's continue.

Resources

← Previous5. `Bundle`: passing bookings between rulesNext →7. A sequence that breaks an invariant