8. Mini-project: three properties of `refund_cents` checked by hand

Description

The time has come to put everything together with your hands. Over seven lessons we took property-based apart into pieces: the limit of the example, the definition of property, how to find them in Reservo, the side-by-side contrast, why the machine catches the weird cases, when the technique pays off. This mini-project is the synthesis: you are going to write three properties of refund_cents yourself and check them by hand over 1000 random inputs, first against the correct implementation —where they must all stay quiet— and then against the uncapped loyalty bonus one —where you are going to see which jumps and which don't. It is the whole module condensed into a single script that runs.

By the end you will have a concrete deliverable: three properties stated precisely, the loop that tests them over 1000 cases, the run that shows everything green against the correct code, the run that shows one property jumping against the broken code, and the minimal counterexample that exhibits the bug. And —this is what really sticks— you are going to verify firsthand the most important lesson of L4: different properties catch different bugs. The three you write are all true, but only one catches the uncapped bonus; the other two stay green against the broken code. Seeing that with your data, not in an explanation, is what turns knowledge into instinct.

Connection with the module: this is the capstone lesson. It doesn't introduce a new concept; it puts you to apply all of the module's in a complete flow, from start to finish, with a deliverable. It is also the last link before the tool: the mini-project ends by building, quite intentionally, the right amount of frustration —the ugly counterexample, the by-hand for, the lack of shrinking— that makes you want Hypothesis. And there we leave you, at the threshold of M2. For the last time we do it by hand, with random; from the next module on, the machine takes the for.

The assignment, in one sentence

Here is your mission, exactly as you would receive it on a real team:

We have refund_cents, the function that decides how much is refunded on cancelling a booking. It handles money, so a bug there costs real cash. Write a property check —three invariants— that watches it over hundreds of random cases, and prove to me that your check works by running it against a version with a known bug and watching it jump.

Note the last part: it is not enough to write properties that pass; you have to prove they can fail. It is the discipline of L7 made a delivery requirement. A property you never saw red is not worth it.

An analogy: the three locks of a single door

Think of the door of a vault with three different locks: a key lock, a combination lock and a fingerprint one. They are not redundant; each defends against a different attack. The key lock stops cold whoever doesn't have the key but does have the combination. The fingerprint one stops whoever copied the key. A thief has to defeat all three, and since each watches a different weakness, together they cover much more than three times the same lock.

Your three properties are those three locks over refund_cents. The range watches that the refund doesn't leave [0, paid]. The monotonicity watches that cancelling earlier never refunds less. The "paid 0 ⇒ refund 0" watches that whoever paid nothing receives nothing. A bug has to respect all three to go unnoticed, and since each looks at a different thing, together they corner correctness much better than any one alone. When you run the check against the uncapped bonus you are going to see, literally, that this bug defeats two locks (monotonicity and paid-zero stay green) but crashes against the third (the range). Without the range lock, the thief would have gotten in.

Step 1: state the three properties precisely

Before touching code, write the three rules in words, in the form "for every valid input, ... holds." This step seems like a formality and it is half the work: a badly stated property produces a useless check.

1. Range. For every price_paid >= 0 and every cancellation instant, the refund satisfies 0 <= refund <= price_paid. (No charge for cancelling; no money given away.) It is a range invariant.
2. Monotonicity. For every price_paid and every pair of instants, if you cancel with more lead time, the refund is not less than if you cancel with less. (Cancelling earlier never harms you.) It is a relationship between inputs.
3. Paid zero ⇒ refund zero. For every cancellation instant, if price_paid == 0, then refund == 0. (Whoever paid nothing receives nothing.) It is a boundary case of the range, elevated to its own rule.

Note that none mentions a concrete output value (nothing about "6000"). The three are rules with "for every," not examples. And the three are falsifiable: you can imagine code that breaks each one (one that refunds too much breaks the range; one that refunds less on cancelling earlier breaks the monotonicity; one that gives a cent with paid zero breaks the third). That falsifiability is what makes them useful and non-trivial properties, as we discussed in L7.

Step 2: write the check by hand

Now the code. A single script that tests the three properties over 1000 cases. For the monotonicity we need two instants per case (an earlier one, a later one); for the third, we evaluate with price_paid = 0. The import at the top is the switch that lets us alternate between the correct implementation and the buggy one without touching anything else.

# check_refund_properties.py — three properties of refund_cents, by hand, 1000 cases
import random
from datetime import datetime, timedelta
from reservo.models import Booking

# Choose ONE of the two lines:
from reservo.refunds import refund_cents        # CORRECT implementation
# from refunds_buggy import refund_cents        # UNCAPPED loyalty bonus

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


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


def refund_at(hours_before, price_paid):
    now = START - timedelta(hours=hours_before)
    return refund_cents(a_booking(), price_paid, now)


range_fail = mono_fail = zero_fail = 0
first_range = None
for _ in range(1000):
    price_paid = random.randint(0, 50_000)
    ha = random.uniform(-10, 200)
    hb = random.uniform(-10, 200)
    early, late = max(ha, hb), min(ha, hb)   # early = more lead time

    r_early = refund_at(early, price_paid)
    r_late = refund_at(late, price_paid)

    # PROPERTY 1 (range): 0 <= refund <= paid
    if not (0 <= r_early <= price_paid):
        range_fail += 1
        if first_range is None:
            first_range = (early, price_paid, r_early)
    # PROPERTY 2 (monotonicity): cancelling earlier never refunds less
    if not (r_early >= r_late):
        mono_fail += 1
    # PROPERTY 3 (paid 0 => refund 0)
    if refund_at(early, 0) != 0:
        zero_fail += 1

print(f"Inputs tested: 1000")
print(f"  P1 range (0<=refund<=paid):       {range_fail} violations")
print(f"  P2 monotonicity (early>=late):    {mono_fail} violations")
print(f"  P3 paid 0 => refund 0:            {zero_fail} violations")
if first_range:
    h, p, r = first_range
    print(f"  First counterexample of P1: {h:.2f} h, paid={p}, refund={r}")

Recognize the three pieces of L3 in the code: the input space (prices from 0 to 50000, hours from −10 to 200, including late cancellations), the generator (random.randint and random.uniform), and the three invariant assertions (the three if not). It is the same anatomy as the whole module, now with three rules in parallel.

Step 3: run against the correct code (the three locks hold)

With the import pointing to reservo.refunds (the good version), run the script.

What to expect. Total silence: the three properties at zero. The correct implementation respects the three rules in the 1000 inputs, including the late cancellations.

$ python3 check_refund_properties.py
Inputs tested: 1000
  P1 range (0<=refund<=paid):       0 violations
  P2 monotonicity (early>=late):    0 violations
  P3 paid 0 => refund 0:            0 violations

Three zeros. It might seem anticlimactic —"I ran 1000 cases to see nothing"—, but it is exactly the signal of confidence you are looking for: you tested three different rules at 1000 points spread across the space, including the weird ones, and none broke them. This is what a good set of properties does against correct code: stay quiet. Keep this run; it is the first half of your deliverable.

But remember the warning from L7: a green that was never red proves nothing. Three zeros against the good code could mean "the properties are strong and the code is correct" or "the properties are trivial and always pass." To tell them apart, you have to see them fail.

Step 4: run against the broken code (one lock gives, two hold)

Change the import: comment out the reservo.refunds line and uncomment the refunds_buggy one (the uncapped loyalty bonus). Nothing else changes. Run again.

What to expect. Here is the project's revelation. The range (P1) explodes with hundreds of violations. But the monotonicity (P2) and the paid-zero (P3) stay at zero, against the very broken code.

$ python3 check_refund_properties.py
Inputs tested: 1000
  P1 range (0<=refund<=paid):       935 violations
  P2 monotonicity (early>=late):    0 violations
  P3 paid 0 => refund 0:            0 violations
  First counterexample of P1: 130.66 h, paid=28113, refund=51165

Stop and savor this result, because it is the whole module's lesson in four lines. The uncapped bonus refunds too much with lots of lead time. That breaks the range (P1): 935 of 1000 cases violate refund <= paid. But look at the other two:

• The monotonicity (P2) stays green because the bonus grows with the lead time —more hours, more bonus, more refund—, so the function remains a staircase that only goes up. The bug doesn't invert the order; it only inflates the values. The monotonicity doesn't see it.
• The paid-zero (P3) stays green because, with price_paid = 0, the bonus 0 + 0 * bonus // 100 still gives 0. The bug multiplies the price paid by a percentage; if the price is zero, there is nothing to inflate. The third property doesn't see it.

This is, with your own data, the moral of L4: a single property almost never suffices. If you had written only the monotonicity, or only the paid-zero, this money bug would have passed green and you would have slept peacefully with a cash leak in production. It was the range property —one of three— that caught it. That is why you write several: each watches a different weakness, and you don't know in advance which one will catch the next bug. Three locks, and the thief crashed against a single one.

Step 5: shrink the counterexample to its minimal form

The loop reported the first counterexample of P1: 130.66 h, paid=28113, refund=51165. It is true but enormous and hard to read —do the 130 hours matter? the odd price? The professional deliverable includes the minimal counterexample, the one that shouts where the bug is. Let's shrink it by hand, reasoning about the code.

The bonus activates as soon as you pass 48 hours. At 49 hours, bonus_percent = int(49 - 48) = 1, so the refund is price + price * 1 // 100. That price // 100 (integer division) only adds a cent when price >= 100. So the smallest case that still exhibits the bug is 49 hours with 100 cents:

$ python3 -c "..."   # evaluating refunds_buggy at three neighboring points
49 h, paid 100 -> 101   (violates: 101 > 100)
49 h, paid 99  -> 99    (doesn't violate: 1% of 99 rounds to 0)
48 h, paid 100 -> 100   (doesn't violate: the bonus is 0 right at the threshold)

The minimal counterexample is 49 hours, paid 100 cents, refunds 101 —a single cent as a gift, barely across the 48-hour threshold. It says exactly the same thing as the 130-hour monster (the bug lives above 48, in the integer division of the bonus), but anyone understands it at a glance: "just past 48 hours, with a price of at least 100, a cent too much is returned." That is the case you bring to whoever has to fix the code.

Note the work it took to reduce it: you had to reason about the arithmetic of the bonus, test neighboring points, find the edge. It is tedious and easy to get wrong. Remember that annoyance —it is the last piece your hand-made check is missing, and the one Hypothesis is going to give you automatically in M5 with shrinking.

The deliverable

Your finished mini-project consists of five things. Gather them; they are the module's product:

1. The three properties stated in words, each in the form "for every valid input, ... holds" (range, monotonicity, paid-zero). — Step 1.
2. The script check_refund_properties.py that checks them over 1000 cases, with the import as a switch between the two implementations. — Step 2.
3. The run against the correct code: three zeros. The evidence that the properties stay quiet when they should. — Step 3.
4. The run against the broken code: P1 with 935 violations, P2 and P3 at zero. The evidence that the check works (it can fail) and that different properties catch different bugs. — Step 4.
5. The minimal counterexample: 49 h, paid 100, refunds 101. The readable diagnosis you hand to whoever fixes it. — Step 5.

With that you fulfilled the complete assignment: you didn't just write properties that pass, you proved they can fail and delivered the minimal case that exposes the bug. That is property-based done with craft, even if still by hand.

Deep dive: what this mini-project left you ready for in M2

Take a step back and look at what you just built, because it is —almost exactly— what Hypothesis does, only by hand. Your script has a generator (random), a set of invariant assertions (the three if not), a loop that runs many cases (1000), and a counterexample report. You added, with human effort, the shrinking to the minimum. Those are, piece by piece, the parts of a professional property-based tool.

Now name what cost you and what you were missing, because it is the sales pitch of M2:

• Writing the generator by hand is tedious and fragile. You had to choose ranges (0 to 50000, −10 to 200), remember to include the late cancellations, generate two instants for the monotonicity. With Hypothesis, you describe the space with strategies (st.integers, st.datetimes) and the tool generates for you, including the edges that your uniform random.uniform almost never produces.
• The uniform generator is blind to point bugs. As you saw in L6, random.uniform almost never hits an exact value like 48.0. Hypothesis's generators seed the extreme values and thresholds on purpose, so they also attack those pin-point bugs.
• Shrinking by hand is a pain. Reducing 130.66 h, 28113 to 49 h, 100 cost you reasoning about the arithmetic. Hypothesis does it alone: it always hands you the minimal counterexample, not the first it stumbled onto.
• Reproducibility you handled with a seed. Hypothesis goes further: it keeps a database of failed examples and re-tests them automatically, so a bug that appeared once never escapes again.

In other words: you understand the engine. You are not going to arrive at M2 to learn a new and mysterious concept; you are going to arrive to replace your by-hand for with a tool that does the same thing, better, and that takes away exactly the tedious parts —the generator, the shrinking, the reproducibility— to leave you the only one that really matters and that no machine does for you: deciding what property your code must satisfy. That skill —the one you practiced in this whole module— is what you take with you. The tool is plumbing around it.

Common mistakes

Writing the three properties but running them only against the good code. Three zeros against the correct implementation don't prove that your properties work; they could be trivial. The assignment requires seeing them fail. If you skip Step 4, you deliver a check you don't know works. The discipline is to always run against both versions: the one that keeps them quiet and the one that makes them shout.

Concluding that the monotonicity and the paid-zero "are useless" because they didn't catch this bug. On the contrary: they work, they just watch other weaknesses. The monotonicity would catch a bug that refunded less on cancelling earlier; the paid-zero would catch one that gave money to whoever didn't pay. That they don't catch this bonus bug doesn't invalidate them —it validates them as different locks. Discarding a property because it didn't catch a concrete bug is like removing the fingerprint lock because today's thief came in through the window.

Delivering the first (ugly) counterexample instead of the minimal one. 130.66 h, 28113 is correct but terrible for debugging: it wastes time on irrelevant details. The case that illuminates the bug is the minimal one, 49 h, 100. Skipping Step 5 hands whoever fixes the code a puzzle instead of a diagnosis. The shrinking is part of the work, even if by hand it costs.

Fixing the price at a comfortable value and generating only the hours. If in the loop you had left price_paid = 6000 fixed and only varied the hours, you would have lost a whole dimension of the space —and a bug that depended on the price (like the rounding of the integer division, which is only seen with small prices) would have escaped you. Generate all the dimensions at once; freezing one at an example value reintroduces the author's bias that property-based came to eliminate.

Exercises

Exercise 1

Add a fourth property to check_refund_properties.py and run it against the two implementations. Proposal: "the refund never exceeds the 100% policy plus a reasonable margin" doesn't work (what margin?), so choose a truly falsifiable one. Hint: think of a relationship between the refund and the price paid that the correct version always satisfies and that the uncapped bonus breaks —different from the range you already have.

# PROPERTY 4: with 48+ hours of lead time, the refund is exactly what was paid
if early >= 48 and refund_at(early, price_paid) != price_paid:
    p4_fail += 1

Exercise 2

The uncapped bonus breaks the range in 935 of 1000 cases with random.seed(1000). Change the hours generator from random.uniform(-10, 200) to random.uniform(-10, 47) —only cancellations of less than 48 hours— and run again against refunds_buggy. How many P1 violations do you expect now? Why? What does it teach you about the relationship between the generator and what a property can catch?

Exercise 3

Invent a new version of refund_cents with a bug different from the uncapped bonus, one that breaks the monotonicity or the paid-zero instead of the range. Write it, run the three-property check against it, and confirm that the corresponding property jumps and the others don't. Hint to break the monotonicity: make the function refund less at a certain hour than at a later hour (invert a tier).

# refunds_inverted.py — breaks the MONOTONICITY (different bug)
def refund_cents(booking, price_paid_cents, now):
    hours_until = (booking.start - now).total_seconds() / 3600
    if hours_until >= 48:
        return price_paid_cents * 50 // 100   # BUG: the most foresighted get less
    if hours_until >= 24:
        return price_paid_cents
    return 0

Summary and next step

You close the module with a complete project in your hands:

• You wrote and checked three properties of refund_cents over 1000 cases: range (0 <= refund <= paid), monotonicity (cancelling earlier doesn't refund less) and paid-zero (paid 0 ⇒ refund 0). Three locks, each watching a different weakness.
• Against the correct code, the three stayed quiet (three zeros). Against the uncapped bonus, only the range jumped (935 violations) while the monotonicity and paid-zero stayed at zero —the demonstration, with your data, that different properties catch different bugs and that a single one almost never suffices.
• You reduced the ugly counterexample (130.66 h, 28113) to its minimal form (49 h, paid 100, refunds 101), the readable diagnosis you hand to whoever fixes it —by hand, with effort.
• The deliverable has five pieces: the stated properties, the script, the green run, the red run and the minimal counterexample. Not just properties that pass: the demonstration that they can fail.
• You built, by hand, almost a whole property-based tool —generator, assertions, many cases, report, shrinking. You know what cost you (the generator, the shrinking, the reproducibility) and that is why you are going to value what the tool automates.

And with this the M1 ends. Review the arc: you started by seeing that example-based tests only cover the cases you thought of (L1-L2), you learned what a property is and its anatomy (L3), how to find them in Reservo (L4), how to contrast them with examples (L5), why the machine catches the weird cases (L6), when the technique pays off (L7) and —here— how to apply it all end to end. You swapped the streetlight for the flashlight, and now you know how to use it by hand.

In Module 2 we drop the homemade for and the tool comes in: Hypothesis. You are going to install it (pip install hypothesis), get to know the @given decorator and the basic strategies (st.integers, st.floats, st.text, st.datetimes), and see the machine do, in two lines, what you did here in twenty —generate hundreds of cases, including the edges, and report the example that falsifies. Everything you understood by hand in this module is the map; M2 gives you the vehicle. See you there.

Resources

• Quick start / @given — Hypothesis (official documentation) — the entry point of M2: how @given replaces your by-hand for loop and generates the cases for you. Read it to see where this mini-project ends up, automated.
• What you can generate and how — Hypothesis (official documentation) — the catalog of strategies (st.integers, st.datetimes, ...) that replace your random.randint/random.uniform, with edges included.
• How Hypothesis works (shrinking) — Hypothesis (official documentation) — the automation of the by-hand shrinking of Step 5: how the tool always hands you the minimal counterexample (49 h, 100) instead of the first it stumbles onto.
• random — Python official documentation — the by-hand generator we use for the last time in this mini-project. random.seed(1000) makes the run reproducible: same 935 counterexamples, always.