Property-Based Testing as a Design Tool

Part 1 – Motivation and Foundations

Property-based testing is a powerful tool for designing correct, unambiguous programs through executable specifications.

It helps us answer an essential question:

What types of universal claims about a program are worth defining and enforcing?

A property is a proposition of the form:

$\forall \; x_1 \in D_1,\; x_2 \in D_2,\; \ldots,\; x_n \in D_n,\; P(x_1,\ldots,x_n)$

where:

• Each $D_i$ represents the domain of discourse for which the operation is defined (the set of possible values for each input parameter).
• $P$ is a logical predicate describing the program’s behaviour.

Property-based tests do not attempt to prove such universal claims.

Instead, they try to falsify them by sampling the input domain in search of counterexamples. A single counterexample is enough to invalidate the claimed property (Popperian philosophy).

The Domains $D_i$ and Generators

Property-based testing needs concrete representations of the domains $D_i$ over which a property is quantified. Generators encode how to sample values from the space of inputs a component operates on.

Property-based tests aim to ensure that properties hold across the entire domain $D_i$, not merely for a curated set of examples.

The randomness in generators serves not to produce random tests, but to increase the chances that the domain is well-sampled. Since sampling can be biased, falsification is only as effective as the generators it depends on.

The quality of a generator directly affects test effectiveness: a missing counterexample in an uncovered region of the domain will remain undetected.

The Predicate $P$

Predicates describe the externally observable behaviour of a component that must remain true: its contract.

They:

• Encode reference implementations, algebraic laws, relations, domain rules.
• Are agnostic to implementation details.

Effective predicates lead to reduced ambiguities and clear understanding of component semantics.

This is particularly valuable when composing components, reasoning about interaction between operations, or designing stateful components, where behaviour emerges from a sequence of actions.

Preconditions

The domain of discourse can be further restricted using implications and preconditions:

$\forall x_1 \in D_1,\; \ldots,\; x_n \in D_n,\; \operatorname{Pre}(x_1,\ldots,x_n) \Rightarrow \operatorname{Post}(x_1,\ldots,x_n)$

Preconditions define the conditions in which a property must always hold, such as valid inputs or states.

They restrict the domain of discourse and may reduce the chances of finding a counterexample if they shrink the input space excessively.

Part 2 – Property-Driven Design in Practice

These ideas become concrete when applied to a real system design.

Suppose we are tasked with building a Scheduling API. Such components provide critical operations: checking availability, detecting overlaps, manipulating time spans, to name a few. Scheduling will be built on top of more fundamental components: discrete intervals.

A sensible first step is to model intervals as ranges of numbers rather than timestamps. A minimal structure consisting of start and end, preserving start < end, may appear sufficient. It rarely is.

This is where ambiguity begins – the unspoken assumptions:

• Does containment include the endpoints?
• When do two intervals intersect?
• Fundamentally: how do interval operations relate to each other?

None of these questions are answered by the data structure alone. I’ve tried extensive documentation (still important, but complementary) as well as large types and function names, without significant improvement.

Ambiguity remained. And worse, it created a false sense of understanding, which eventually led to unpredictable behaviour, particularly when composing operations.

Domain Pressure Trims the Design

Scheduling systems care about overlapping, adjacency, ordering, containment of time spans.

Rather than trying to encode the complete theory of intervals, the Interval API is restricted to the set of operations required to express and support schedule invariants.

Domain-Driven Interval Properties

The following tables map required scheduling features to the interval semantics needed to support them, and the corresponding properties that enforce them.

Validity and Error Modes

Components are expected to reject, sanitise or fail fast when the input is invalid.

Conflicts & Coexistence

Scheduling systems must detect overlapping schedules to detect conflicts, allow new disjoint ones to coexist, handle overrides.

Continuity, Adjacency and Gaps

Schedule systems need to understand if schedules are back-to-back (adjacent) or if there is room for new ones between them.

Partial Order

Ensuring that contains forms a partial order enables safe composition, local reasoning about nested structures (avoiding examining entire hierarchies), and defines proper equality semantics.

A Few Curated Examples

Four Interval Types, One Consistent API

Grouping the properties that must hold across all interval types goes beyond DRY. It is a powerful tool for designing unified APIs with consistent, well-defined semantics.

  checkIntervalProperties("closed", Intervals.makeClosed[Int])
  checkIntervalProperties("open", Intervals.makeOpen[Int])
  checkIntervalProperties("half-open right", Intervals.makeHalfOpenRight[Int])
  checkIntervalProperties("half-open left", Intervals.makeHalfOpenLeft[Int])

Crucially, not all operations are total: some are undefined for certain interval types. For example, adjacency has no meaning for open intervals, because open intervals have no boundary points.

Property-based testing must navigate this partial landscape enforcing laws only where operations are defined.

Encoding Validity Through Construction

Smart constructors (makeClosed, makeOpen, and similar factory functions) ensure that only intervals satisfying their invariants can be constructed.

The behaviour of interval smart constructors is specified using implications:

This states that construction must succeed whenever the validity precondition holds.

In practice, instead of encoding this implication directly in the tests, we restrict the generator to produce only inputs satisfying the precondition.

This preserves the specification while increasing the chances of falsification and making the domain of discourse explicit.

    property(s"$name intervals are valid"):
      forAll(properBounds) { case (start, end) =>
        val result = factory(start, end)
        alg.validBounds(result.start, result.end) &&
        result.start == start &&
        result.end == end
      }

Conversely, when the input is invalid, the smart constructor must not construct an interval.

In this design, invalid inputs result in immediate error rather than a recoverable value (such as Option or Either): trying to create an interval is considered a bug, not a valid use case.

    property(s"$name intervals reject invalid bounds"):
      forAll(reversedBounds) { case (start, end) =>
        throws(classOf[IllegalArgumentException]) {
          factory(start, end)
        }
      }

Together, these two properties specify the observable success and failure behaviour of interval construction over the domain of bounds.

Domain-Specific Generators

In the IntervalSpec, most interval properties are defined over specific domain subsets, rather than through implications and preconditions. For example:

These properties require custom generators that sample directly from the relevant domain of discourse ($\mathcal{I}_{\text{disjoint}}$ in this case), rather than relying on implications and on discarded invalid samples.

Examples of such interval generators include: properIntervals, adjacentIntervals, intersectingIntervals, and disjointIntervals.

Non-Total Properties and Vacuous Truth

Adjacency is not defined for all interval types. In particular, it is undefined for open intervals: for example, the open intervals (6, 7) and (7, 8) are not adjacent since they do not share a boundary point.

Rather than expressing adjacency laws through implications, we can define them over a restricted domain:

This formulation also holds for open intervals, but only vacuously. When $\mathcal{I}_{\text{adjacent}} = \emptyset$, the property still holds, since $\forall x \in \emptyset,\; P(x) \equiv \text{true}$.

We can encode this behaviour directly in the generator. The adjacentIntervals generator produces:

• Some((a,b)) when a pair of adjacent intervals exists (closed or half-open intervals)
• None when adjacency is undefined (open intervals).

The property can then be written as:

    property(s"adjacent $name intervals never intersect"):
      // Vacuously true when no adjacent intervals exist
      forAll(adjacentIntervals) { adjs =>
        adjs.forall { case (a, b) => a.isAdjacent(b) && !a.intersects(b) }
      }

Relationships, Implications and Vacuity

Some relationships between operations are inherently conditional.

For example, consider the relationship between containment and intersection: if an interval contains another, they intersect. Formally:

In such cases, tests are often expressed as implication. Using De Morgan’s laws, implications can be rewritten into a form more suitable for programming languages:

However, such implication-based properties are prone to vacuous truth and may convey no information at all if the antecedent rarely holds.

property(s"containing intervals intersect for $name intervals"):
  forAll(properIntervals, properIntervals) { case (a, b) =>
    // a.contains(b) ⇒ a.intersects(b)
    !a.contains(b) || a.intersects(b)
  }

If !a.contains(b) always evaluates to true, the test will always succeed, even if a.intersects(b) is broken. This typically occurs when the generator rarely produces input satisfying the antecedent.

Takeaway

Through this lens, property-based testing is not primarily about testing. It is about deliberately constraining API semantics to what the domain demands.

Collapsing an unbounded space of possible behaviours into a small set of precise properties is difficult – but necessary. Ambiguous components do not compose into reliable systems.

Deadlines and pressures are real, but core quality cannot be negotiated. Some parts of a system must be correct, predictable, and composable by design.

The goal is to build systems that fulfill their objectives. Property-based testing is one of the best tools for designing the composable and predictable components that make this possible.

Links

• Interval | IntervalSpec | IntervalGens