Property Based Testing - Induction

Introduction

Property-based testing is a leap forward from traditional example-based tests. With tools like pytest and hypothesis, we can verify our code’s behavior over a massive, randomized set of inputs. But what if we could go even deeper? What if, instead of just testing outputs, we could test the rules of our algorithm itself?

This is where a classic proof technique from mathematics, mathematical induction, provides an incredibly powerful mental model. By structuring our property-based tests to mirror induction, we can achieve a more profound level of confidence, verifying that the structural integrity of our code holds, no matter how large the input grows.

The Theory: Mathematical Induction

Before we dive into code, let’s understand the core concept in its formal terms. In mathematics, proof by induction is a formal proof technique used to establish that a given statement P(n) is true for all natural numbers n (or all numbers from a certain starting point). A proof by induction consists of two distinct steps:

  1. The Base Case (or Basis): We prove that the statement holds for the first or simplest case, typically $n=0$ or $n=1$. This establishes a foundation for the proof, written as proving $P(0)$.

  2. The Inductive Step: We prove that if the statement holds for some arbitrary case $n=k$, then it must also hold for the next case, $n=k+1$. The assumption that $P(k)$ is true is called the Inductive Hypothesis. This step is written as proving that for all $k$, the implication $P(k) \implies P(k+1)$ is true.

This two-step process can seem abstract, but it has a simple, intuitive parallel: a line of falling dominoes. The base case is proving you can knock over the first domino. The inductive step is proving that if any given domino falls, it has enough momentum to knock over the next one in line. If both of these conditions are true, you can conclude with certainty that all the dominoes will fall, no matter how long the line is.

In programming, we can adapt this powerful structure. Instead of proving a property for all numbers, we use it to verify that our code’s logic is sound for inputs of any valid size.

From Theory to Practice: The Inductive Testing Pattern

The structure of an inductive proof maps beautifully to pytest and hypothesis. We can write two distinct tests for any pure function that follows this pattern:

  1. A test for the Base Case(s). This establishes our “first domino” using a simple, hardcoded assertion.

  2. A test for the Inductive Step. This verifies the “chain reaction” using hypothesis to generate arbitrary inputs and check if the rule holds between one size and the next.

Let’s see this in action with common Python built-in functions, ordered from simplest to most conceptually complex.

Example 1: sum()

This is the canonical example. Its inductive property is simple and clear: the sum of a list is the sum of its first $n-1$ elements plus the last element.

# The function we are testing
from builtins import sum
from hypothesis import given, strategies as st
Base Case

The simplest case for sum() is an empty list, which should equal 0.

def test_sum_base_case():
    """Base Case: The sum of an empty list is 0."""
    assert sum([]) == 0
Inductive Step

We verify the recursive property by generating a list and a new element.

@given(
    st.lists(st.integers()),
    st.integers(),
)
def test_sum_inductive_step(lst, elem):
    """
    Inductive Hypothesis: We assume `sum(lst)` is correct.
    Inductive Step: We prove that summing a new list is equal to the
    sum of the old list plus the new element.
    """
    assert sum(lst + [elem]) == sum(lst) + elem

Example 2: pow(x, y)

Exponentiation is another classic recursive function: for a positive integer exponent $y$, we can define $x^y$ as $x \times x^{y-1}$.

# The function we are testing
from builtins import pow
Base Case

The base case for exponentiation is that any number to the power of 0 is 1.

def test_pow_base_case():
    """Base Case: Any number to the power of 0 is 1."""
    assert pow(2, 0) == 1
Inductive Step

We verify the multiplicative property for positive integer exponents.

@given(
    st.integers(min_value=1, max_value=100),
    st.integers(min_value=1, max_value=100),
)
def test_pow_inductive_step(x, y):
    """
    Inductive Hypothesis: We assume `pow(x, y - 1)` is correct.
    Inductive Step: We prove that `pow(x, y)` is `x` times the
    result of the smaller power.
    """
    assert pow(x, y) == x * pow(x, y - 1)

Example 3: str.join()

This example moves from pure arithmetic to string manipulation. Joining a list of strings has a perfect inductive structure. The result of joining $n$ strings is the result of joining $n-1$ strings, followed by the separator and the $n$-th string.

Base Case

The simplest cases are joining an empty list or a single-element list.

def test_join_base_cases():
    """Base Cases: Test joining with zero and one element."""
    assert ",".join([]) == ""
    assert ",".join(["a"]) == "a"
Inductive Step

We verify the concatenation property for any list with at least one item.

@given(
    st.lists(st.text(), min_size=1),
    st.text(),
)
def test_join_inductive_step(lst, elem):
    """
    Inductive Hypothesis: `','.join(lst)` is correct.
    Inductive Step: The full join is the partial join plus the
    separator and the last element.
    """
    separator = ","
    assert separator.join(lst + [elem]) == separator.join(lst) + separator + elem

Example 4: min() and max()

This example’s simplest meaningful case is a two-element list, which distinguishes the two functions.

# The functions we are testing
from builtins import min, max
Base Cases

We use a simple hardcoded list with two distinct numbers.

def test_min_base_case():
    """Base Case: For two elements, min() returns the smaller one."""
    assert min([10, 5]) == 5

def test_max_base_case():
    """Base Case: For two elements, max() returns the larger one."""
    assert max([10, 5]) == 10
Inductive Steps

For a list of one or more elements, the recursive property holds.

@given(
    st.lists(st.integers(), min_size=1),
    st.integers(),
)
def test_min_inductive_step(lst, elem):
    """
    Inductive Hypothesis: We assume `min(lst)` is correct.
    Inductive Step: `min` of a larger list is the min of the
    smaller list's min and the new element.
    """
    assert min(lst + [elem]) == min(min(lst), elem)

@given(
    st.lists(st.integers(), min_size=1),
    st.integers(),
)
def test_max_inductive_step(lst, elem):
    """
    Inductive Hypothesis: We assume `max(lst)` is correct.
    Inductive Step: `max` of a larger list is the max of the
    smaller list's max and the new element.
    """
    assert max(lst + [elem]) == max(max(lst), elem)

Example 5: collections.Counter

This final example introduces a more complex data structure. A Counter object aggregates counts, and its inductive step involves what looks like a stateful update.

from collections import Counter
Base Case

The simplest case is a counter from an empty sequence.

def test_counter_base_case():
    """Base Case: A Counter from an empty list is empty."""
    assert Counter([]) == Counter()
Inductive Step

We verify that creating a Counter from a list is equivalent to creating one from a smaller list and then updating it with the final element.

@given(
    st.lists(st.text(min_size=1)),
    st.text(min_size=1),
)
def test_counter_inductive_step(items, item):
    """
    Inductive Hypothesis: `Counter(items)` is correct.
    Inductive Step: The counter of a new list is equivalent to the
    counter of the old list updated with the new item.
    """
    partial_counter = Counter(items)
    partial_counter[item] += 1
    
    assert Counter(items + [item]) == partial_counter

The “Aha!” Moment: Connecting the Dots

Let’s explicitly map the formal concepts of induction to the tests we just wrote.

Mathematical ConceptHow It Appears in Our Tests
Base CaseThe test___base_case() functions. They test the simplest meaningful input ($P(0)$), establishing a “ground truth” to build upon.
Inductive HypothesisThe assumption that the function works for a smaller input ($P(k)$). In test_sum_inductive_step, the call sum(lst) embodies this.
Inductive StepThe assert statement in the test___inductive_step() function. It verifies that the structural rule ($P(k) \implies P(k+1)$) holds.

The most profound shift here is moving from testing outputs to testing relationships. A traditional test asserts factorial(5) == 120. An inductive test asserts factorial(5) == 5 * factorial(4), which is a far more powerful statement about the function’s internal logic. It verifies the algorithm itself.

Let’s summarize how this pattern applies to each function we’ve tested:

Function TestedBase Case ($P(0)$)Inductive Step ($P(k) \implies P(k+1)$)
sum()The sum of an empty list is 0.sum(list + [item]) == sum(list) + item.
pow(x, y)A number to the power of 0 is 1.pow(x, y) == x * pow(x, y-1).
str.join()Joining zero or one item works correctly.Joining n items is equivalent to joining n-1 items, then adding the separator and the last item.
min()The min of two elements is the smaller one.min(list + [item]) == min(min(list), item).
max()The max of two elements is the larger one.max(list + [item]) == max(max(list), item).
collections.CounterA Counter of an empty sequence is empty.The Counter of a list is a Counter of its sublist, updated with the last element.

From Theory to the Trenches: A Remark on Practicality

It is worth noting where these powerful ideas originate. The testing method—property-based testing—was popularized by the QuickCheck library from the functional programming language Haskell. The proof structure—induction—comes from pure mathematics.

However, these techniques are not confined to the functional paradigm or mathematical theory. Their true power is revealed when applied to everyday, non-mathematical, and even non-functional code.

Imagine you have written a highly optimized sorting or aggregation function in Rust, Cython, or C++. You can expose that function to Python via bindings and then test its correctness using this beautifully succinct style. This creates a powerful separation of concerns:

  • Low-Level Code: Worries about performance, memory, and raw computation.

  • High-Level Test: Worries exclusively about correctness in a declarative, readable way.

This approach minimizes the number of manual test cases you need to write while maximizing logical coverage of your algorithm. It is a testament to how abstract concepts from mathematics and computer science can become potent, practical tools in the hands of any programmer.

Conclusion

Property-based testing is already a huge leap forward from example-based testing. By adding the mental model of mathematical induction, you can take it a step further. This approach encourages you to identify the core recursive properties and invariants of your code, leading to tests that are more robust, more expressive, and far better at catching subtle logical flaws.

Next time you are working with a function that builds up a result incrementally or recursively, don’t just test random inputs. Separate the base case from the inductive step, and test the very rule that makes your function work.

Annex: Unleashing the Full Power of Property-Based Testing

The examples in the main article use hardcoded values in their base cases to keep the focus on the inductive structure. While excellent for teaching, a core principle of property-based testing is to eliminate “magic values” and test properties over a wide range of inputs. This annex shows how to convert our hardcoded tests into more powerful, generalized property-based tests.

Generalizing pow()’s Base Case

Instead of testing pow(2, 0), we can assert that pow(x, 0) is 1 for any integer x.

@given(st.integers())
def test_pow_base_case_generalized(x):
    """Base Case: Any number to the power of 0 is 1."""
    assert pow(x, 0) == 1
Generalizing str.join()

We can use pytest.parametrize for the simple base cases and also randomize the separator in the inductive step to make it more robust.

import pytest

@pytest.mark.parametrize("lst, expected", [
    ([], ""),
    (["a"], "a"),
])
def test_join_base_cases_parametrized(lst, expected):
    """Base Cases: Test joining with zero and one element."""
    assert ",".join(lst) == expected

@given(
    st.text(),
    st.lists(st.text(), min_size=1),
    st.text(),
)
def test_join_inductive_step_generalized(separator, lst, elem):
    """Inductive Step: Test with any separator."""
    assert separator.join(lst + [elem]) == separator.join(lst) + separator + elem
Generalizing min() and max() Base Cases

Instead of a single example like [10, 5], we can generate any two integers and check the property.

@given(st.integers(), st.integers())
def test_min_base_case_generalized(a, b):
    """Base Case: For any two elements, min() returns the smaller one."""
    expected = a if a <= b else b
    assert min([a, b]) == expected

@given(st.integers(), st.integers())
def test_max_base_case_generalized(a, b):
    """Base Case: For any two elements, max() returns the larger one."""
    expected = a if a >= b else b
    assert max([a, b]) == expected
A Note on Fixed Base Cases

For functions like sum() and Counter, the base case is a single, fixed identity element (0 and an empty Counter, respectively). In these scenarios, the hardcoded base case is already the most general and correct form, so no change is needed. This demonstrates that the goal is not to eliminate all hardcoding, but to replace arbitrary examples with generalized properties wherever possible.