Module 1: From Examples To Properties

3. What a property is (an invariant)

Next →

Description

You already know that an example covers one point and that this leaves the input space almost entirely untested. It is time to define precisely the tool that sweeps that space: the property. The word is used a lot and loosely, so we are going to pin it down rigorously, because half the errors when starting with property-based come from a blurry definition.

By the end of this lesson you will be able to say, without hesitation, what a property is and how it differs from an example: a property is an assertion with a universal quantifier —"for EVERY valid input X holds"— where X is a verifiable rule, not a concrete value. You will get to know the word at the heart of the matter, invariant (something that doesn't change no matter how much the inputs change), and you will learn the anatomy of every property check, which always has the same three pieces: an input space, a generator that samples it and an assertion of the invariant. With those three pieces named, you will be able to read and write properties without getting confused, here by hand and —from M2— with Hypothesis.

Connection with the module: this is the definitions lesson. L2 left you with the gap clearly seen; this one gives you the concept that fills it. We are not going to search for properties in Reservo yet (that is L4) nor put them against the examples (L5); here we build the conceptual and code scaffolding that those lessons take for granted. If this lesson is clear to you, the next three will feel like applying a template.

An analogy: the cashier's rule against the receipt

Think of two ways of controlling a store's register. The first is to review concrete receipts: "the 3:47 receipt says Ana paid 250 pesos for two coffees; is the sum right?" You verify a receipt, a case, a point. It is an example.

The second is to impose a rule that every receipt must satisfy, no matter who buys or what: "the total of any receipt equals the sum of its line items, and it is never negative." That rule doesn't talk about Ana or about 3:47; it talks about all possible receipts, yesterday's, today's and the ones that don't exist yet. If one day a receipt appears that violates it —a negative total, or a total that doesn't match its line items—, you know something broke, even though you would never have imagined that particular receipt.

A property is that cashier's rule. It doesn't verify a receipt; it states a truth every receipt must respect, and then it searches for one that doesn't. The example looks backward, at a case that already happened; the property looks toward all cases, including the ones that don't occur to you. That is the difference in altitude between the two, and that is why a single well-placed property is worth infinite receipts reviewed by hand.

The definition, piece by piece

Let's go to the formal definition, and then we take it apart.

A property is an assertion of the form "for every valid input x, P(x) holds", where P is a condition that can be evaluated as true or false.

Three words carry all the weight. Let's look at them.

"For every" — the universal quantifier. This is what separates a property from an example. An example says "for this input." A property says "for every input." It is not a nuance: it is a leap from a point to a complete space. When you write or read a property, look for that "for every" in front, explicit or implicit. If it is not there, it is not a property; it is an example in disguise.

"Valid input" — the domain. The "for every" doesn't literally cover anything at all, but every input within the function's domain. refund_cents expects a price paid that is a non-negative integer (paying −500 cents doesn't exist) and an instant now. A negative price is not a valid input; it is outside the function's contract. Defining the domain well —which inputs are legitimate— is half the work of a property, and it is a topic M3 develops in depth with assume() and strategies that describe exactly the valid space. For now keep in mind that "for every valid input" is not "for any garbage": it is "for everything the function promises to handle."

"P(x) true or false" — the invariant. The condition has to be something you can evaluate and that yields a boolean: 0 <= refund <= price_paid gives True or False. A vague condition ("the refund is reasonable") or a concrete value ("the refund is 6000") doesn't count. It has to be a checkable rule that holds for all the x. That rule that stays constant while the inputs change is called an invariant, and it is the word worth getting tattooed.

Invariant: the key word

An invariant is a property of the system that stays true no matter what happens with the inputs. "In-variant": that doesn't vary. The refund can be 0, 3000, 6000 or anything depending on the hour and the price —that varies—, but the assertion "the refund is between 0 and what was paid" never varies: it holds for every valid input. That is the invariant.

The habit of thinking in invariants is, perhaps, the most transferable skill in all of property-based testing. When you look at a function, instead of asking "what does it return for this input?", you are going to ask "what is true of its output no matter what happens with the input?". The answers to that second question are your properties. And they are surprisingly rich: almost any function has several hidden invariants you never formulated because confirmation mode didn't push you to look for them.

The anatomy of a property check

Every verification of a property —by hand in this module, with Hypothesis from M2— has exactly three pieces. Name them once and you will recognize them forever.

  1. The input space. The set of all valid inputs. For refund_cents: all pairs (price paid ≥ 0, cancellation instant). It is enormous, almost always infinite.
  2. The generator. The mechanism that produces concrete inputs from the space to test them. By hand we use random: random.randint(0, 50_000) for the price, random.uniform(0, 200) for the hours. With Hypothesis, the strategies (st.integers, st.floats, ...) fulfill this role, and much better. The generator is what turns "for every input" (impossible to evaluate literally) into "for these 500 sampled inputs" (evaluable).
  3. The invariant assertion. The assert (or the if not ...) that checks P(x) on each generated input. It is the cashier's rule applied to each receipt.

When you see any property-based test, mentally split it into these three pieces. If something doesn't work, the problem is almost always in one of them: the space badly defined (you let garbage in, or excluded valid cases), the generator narrow (it doesn't cover the interesting zones, as you saw at the end of L1) or the invariant badly written (a rule that always passes, or that doesn't capture what you think). Having the three pieces named gives you a diagnostic checklist.

Worked example: an invariant that holds, verified by hand

So far we have seen properties catching bugs. It is just as important to see a property holding, so it is clear it is not a failure machine: it is a machine for verifying a rule, that stays quiet when the rule is respected. We take the correct implementation of refund_cents and verify the range invariant over hundreds of generated inputs.

Here is the correct implementation, the one from fundamentals:

# reservo/refunds.py — the correct version
def refund_cents(booking, price_paid_cents, now):
    """Refund based on the lead time from now until booking.start."""
    hours_until = (booking.start - now).total_seconds() / 3600
    if hours_until >= 48:
        return price_paid_cents
    if hours_until >= 24:
        return price_paid_cents * 50 // 100
    return 0

And the property check, with its three pieces noted in the comments so you can see them:

# check_invariant.py — anatomy of a property check
import random
from datetime import datetime, timedelta
from reservo.models import Booking
from reservo.refunds import refund_cents   # the CORRECT version

START = datetime(2026, 3, 10, 12, 0)
random.seed(101)


def a_booking():
    return Booking(id="bk", room_id="r", member_id="m",
                   start=START, end=START + timedelta(hours=2))


failures = 0
for _ in range(500):
    # PIECE 1 and 2: the input space, sampled by the generator.
    price_paid = random.randint(0, 50_000)        # valid price: integer >= 0
    hours_before = random.uniform(-10, 200)        # even cancelling late (now > start)
    now = START - timedelta(hours=hours_before)

    refund = refund_cents(a_booking(), price_paid, now)

    # PIECE 3: the invariant assertion.
    if not (0 <= refund <= price_paid):
        failures += 1
        print(f"COUNTEREXAMPLE: paid={price_paid}, {hours_before:.2f} h, refund={refund}")

print(f"Cases tested: 500 | invariant violations: {failures}")

Note a deliberate detail of the generator: random.uniform(-10, 200) includes negative values of hours_before, that is, cancellations after the booking started (now later than start). It is a case almost nobody would write by hand —"cancel a booking that already began"— and it is exactly the kind of corner a property must cover. We want to know whether the invariant holds there too.

What to expect. Silence and zero. The invariant holds for the 500 inputs, including the late cancellations: when now is later than start, hours_until is negative, it falls into the return 0 tier, and 0 is within [0, price_paid]. The rule holds.

$ python3 check_invariant.py
Cases tested: 500 | invariant violations: 0

Not one counterexample line, and a clean 0 at the end. This is what a property does when the code is correct: nothing visible. It may seem anticlimactic —"I ran 500 cases to see nothing?"—, but it is precisely the signal of confidence you are looking for. You tested the invariant at 500 points spread across the space, including the weird ones, and none of them broke it. Compare it with the three comfortable points of L2: the same apparent calm, much more evidence behind it.

Deep dive: a property is both weaker and stronger than an example

There is a useful paradox worth understanding. A property is, in one sense, weaker than an example, and in another sense, stronger. It sounds contradictory; it is not.

It is weaker because it asserts less about each point. The example "72 hours → 6000" tells you the exact value: 6000, not 5999 or 6001. The property "0 ≤ refund ≤ paid" doesn't tell you the value; it only tells you a range. A function that at 72 hours returned 5999 would pass the property (5999 is in the range) and fail the example. In that sense, the property is less demanding at each point: it accepts any value within the band.

And at the same time it is stronger because it asserts something about all the points, not just one. The example says nothing about 71 hours, nor about 73, nor about a price of 9886; the property says something about the three and about infinite more. It covers in breadth what it sacrifices in precision.

From here comes the practical lesson that already appeared and is worth engraving: properties and examples don't compete; they complement each other. Examples contribute point precision (the exact value at key points, the anchor numbers that document the rule). Properties contribute coverage of the whole space (the valid band everywhere). A mature suite uses examples to nail "72 h → 6000, 36 h → 3000, 12 h → 0" and properties to guarantee "and never, ever, at any point, does the refund leave [0, paid] or stop being monotonic." The weakness of one is the strength of the other.

This also explains why a property alone can pass with an absurd function. "0 ≤ refund ≤ paid" is satisfied by a function that always returns 0 —it is within the range at every point—, even though that function is clearly broken (it never refunds someone who cancelled with three days of lead time). The range property doesn't catch it because it doesn't talk about concrete values. That is why you need several properties (range, monotonicity, "paid 0 ⇒ refund 0", which combine to close the ring) and some examples that pin the values. No single tool suffices; the skill is in combining them, and to finding the right set of properties we dedicate L4 and all of M4 later on.

Common mistakes

Confusing "property" with "test that uses parametrize." A parametrize table with twenty rows is still twenty examples: twenty hand-picked points, without "for every." The property is not defined by the number of cases or by the syntax, but by the universal quantifier and the generation. A test with a single assert inside a loop that generates inputs is a property; a table of a thousand hand-written rows is not.

Writing an invariant that is actually a concrete value. "The refund at 72 hours is 6000" is not an invariant, it is an example, even if you put it in a loop. An invariant doesn't mention a fixed output value; it mentions a relationship that holds for all (range, order, equality between two ways of computing). If your "property" contains a magic output number, it is almost surely an example in disguise.

Forgetting to define the domain and letting invalid inputs in. If your generator produces negative prices and your function doesn't promise to handle them, you are going to see "failures" that are not bugs of the function, but inputs outside its contract. "For every valid input" includes the word valid for a reason. Defining the domain —and filtering out what is left out— is part of the property, not a detail. M3 dedicates whole tools to it (assume, bounded strategies).

Believing a green property proves correctness. A single property almost never captures all the correctness (remember the function that always returns 0). Green on a property means "this rule is respected at the points I tested," not "the function is correct." Correctness is cornered with a set of properties plus some examples, never with an isolated rule.

Exercises

Exercise 1

For each phrase, decide whether it is a legitimate invariant (a checkable rule with "for every") or not (because it is an example in disguise, a concrete value or a non-checkable condition). Justify.

  1. "price_cents never returns a negative number."
  2. "price_cents(Focus, pro, 3) returns 6000."
  3. "The price from price_cents is reasonable."
  4. "For the same room and the same hours, the pro price is less than or equal to the basic one."
View solution
  1. Legitimate invariant. "For every room, member and hours, price_cents(...) >= 0." Checkable rule, universal quantifier, no magic values. It is the non-negativity invariant.
  2. Not an invariant. It is an example: a concrete input with an exact output (6000). Useful as a test, but not a property.
  3. Not an invariant. "Reasonable" is not checkable; it doesn't evaluate to True/False objectively. To turn it into a property you would have to make it precise ("it is between 0 and the list price," for example).
  4. Legitimate invariant. "For every room and hours, price_cents(room, pro, hours) <= price_cents(room, basic, hours)." It is a relationship with a universal quantifier; it is called a metamorphic property and you will see it in L4. Note that it doesn't mention any concrete output value: it talks about the relationship between two outputs.

Exercise 2

Reproduce check_invariant.py from this lesson against the correct implementation of refund_cents and confirm the zero violations. Then change a single line —the import— to point to refunds_buggy (the uncapped bonus) and run again. Without executing yet: do you expect zero violations too, or do you expect counterexamples? Why? Then run it and confirm.

View solution

Against the correct version, zero violations (silence and 0), as in the lesson: the range invariant is respected in the 500 inputs, including the late cancellations.

Against refunds_buggy you expect counterexamples, and many. The generator uses random.uniform(-10, 200), so it produces plenty of lead times greater than 48 hours, exactly the region where the uncapped bonus refunds too much and breaks refund <= price_paid. On running it you will see several COUNTEREXAMPLE: lines and a high violation count. It is the same invariant, the same anatomy, different code: the property stays quiet with the correct one and shouts with the broken one. That contrast —not the silence or the shout separately— is what makes it a good test.

Exercise 3

Choose a function of yours or a known one (for example, Python's sorted(list), which sorts a list) and state in writing three invariants of its output, in the form "for every valid input, ... holds." Don't program them; just state them carefully, avoiding concrete values.

View solution

For sorted, three classic and well-formed invariants:

  1. Order. For every input list, the returned list is sorted from smallest to largest: each element is less than or equal to the next.
  2. Length. For every input list, the returned list has the same number of elements as the input one (sorting neither adds nor removes).
  3. Permutation (same elements). For every input list, the returned list contains exactly the same elements as the input one, just rearranged —none appears out of nowhere or disappears.

Note three things. First: none mentions a concrete list or an exact result; all are rules with "for every." Second: the three together corner correctness much better than one alone —the order invariant by itself would be satisfied by a function that always returns [] (an empty list is "sorted"), but that function violates length and permutation. Third: this is exactly the pattern you will apply to refund_cents in the module's mini-project. Searching for several invariants that cover the gaps between each other is the central craft of L4.

Summary and next step

The essentials of this lesson:

  • A property is an assertion with a universal quantifier: "for every valid input x, P(x) holds," where P is a checkable rule, not a concrete value.
  • Three words define it: "for every" (the leap from point to space), "valid input" (the function's domain) and a P(x) true or false (the invariant).
  • An invariant is what doesn't change no matter how much the inputs change: the refund varies, but "it is between 0 and what was paid" doesn't vary. Thinking in invariants is the most transferable skill of property-based.
  • Every property check has three pieces: input space, generator and invariant assertion. Name them and you will have a diagnostic checklist.
  • We saw it hold: the range invariant of the correct refund_cents passed clean over 500 inputs, including late cancellations. A property is not a failure machine; it is a machine for verifying a rule, that stays quiet when it is respected.
  • A property is weaker (it doesn't pin the exact value) and stronger (it covers the whole space) than an example. They don't compete: they complement each other. And a single property rarely suffices; you combine several plus some examples.

You already have the definition and the anatomy. Now the craft part is missing: learning to find the properties hidden in a function you already know, because stating them well is harder than writing an example. That is exactly what's next.

In the next lesson we go out to hunt properties in Reservo. You are going to see three patterns that appear over and over —the range invariant and the monotonicity of refund_cents, the symmetry of overlaps, the metamorphic of price_cents— and you are going to verify them over hundreds of random cases. It is where the theory of this lesson turns into an instinct for looking at code. Let's continue.

Resources

← Previous2. The limit of the example-based testNext →4. The properties hidden in Reservo