Property-based Testing For The Rest Of Us - It's properties all the way down

Arialdo Martini — 10/08/2023 — tdd functional programming property-based testing

Index

  1. Utterly opinionated introduction to Property Testing
  2. Shut up and code!
  3. It’s properties all the way down
  4. Property-driven Development

It’s properties all the way down

A matter of naming

I’ve always suspected that the low adoption of TDD might be partly due to its poor naming. Some developers who never practiced TDD find it counterintuitive that they are supposed to write a test for an implementation even before that implementation exists. How can you blame them? It really sounds crazy.

If only tests were presented as requirements expressed with code, the same skeptic developers would probably find TDD completely natural: of course you produce the code only after the requirements! Of course it would be absurd to write requirements as an afterthought.
If TDD was called Requirement-Driven Design, maybe there would be less resistance to the approach.

Along these lines, I think it would be fair to call TDD “Example-Driven Development”, and PBD “Requirement-Driven Development”.

This leads us to the definition of “Property”, which I intentionally pushed back as much as possible. Before, I wished you to build an intuition of what PBT was really about.

Properties

A Property is an observation on a piece of code that we expect to hold true regardless of the inputs.

To a certain extent, an assertion in TDD is a property that holds for a specific input. Take this case:

record Product(Guid Id, string Name, Category Category, decimal Price);

[Fact]
void books_can_be_shipped_internationally()
{
    var product = new Product(
        Id: Guid.NewGuid(),
        Name: "The Little Schemer", 
        Category: Books, 
        Price: 16.50M);
    
   
    var canBeShipped = Ship(product, Countries.France);
	
    Assert.True(canBeShipped);
}

The property here is

The book 'The Little Schemer' can be shipped to France

or if you like

∃ Product "The Little Schemer" ∈ Books | it can be shipped`


In PBT the property is extended to

All the books can be shipped to France

or equivalently

∀ Product ∈ Books => it can be shipped

which translates to:

[Property]
Property all_books_can_be_shipped_to_France()
{
    Gen<Product> books = 
        Arb.Generate<Product>()
        .Where(p => p.Category == Books);

    bool canBeShippedToFrance(Product product) =>
        Ship(product, Countries.France) == true;

    return Prop.ForAll(books, canBeShippedToFrance);
}

Playing with mathematical terms, one could say that

  • TDD resorts to Existential Quantified Properties: “it exists () an example for which a property holds
  • PBT uses Universally Quantified Properties: “for all the values () this property holds”.
    No surprises that many PBT libraries define a function called forAll, and that the FsCheck’s logo is a .

Besides Existential and Universally Quantified properties, there is another dimension along which you can distinguish what I call the Essential and the Collateral Properties.

  • An Essential Property is the direct translation of the business requirement, like the example of the shipped books.
    Alternative names are Obvious Property and Business Rule as Property. You can read a Java example in Johannes Link’s Pattern: Business Rule as Property

  • A Collateral Property is any observation that holds true in a context, and that can be indirectly deriveded from the business requirement. For example:

    • the fact that sum(a, b) is commutative
    • the observation that sorting a collection does not change its size (a so called “invariant”)
    • the fact that in a bank transfer the sum of money between the two involved bank accounts remains constant (again, an invariant)
    • comparing your program’s behavior with an Test Oracle, that is an alternative, simpler and predictable implementaion of the function under test (see Test Oracle on Wikipedia)
    • running both your system and a simplified model with the same randomized series of input values, and comparing the output and the state. This is called Model-based testing and it is particularly powerful for stateful applications. There are entire article series dedicated to it.

Collateral Properties don’t directly capture the requirements, but derive from them.
Also, in general they don’t completely specify the behaviour of the code under test: usually you need a set of them to form a complete specification.

Collateral Properties are so popular in PBT — and in Design by Contract — that one could think they are specific to it. There is the myth that developers must rack their brains to tranlate business requirements to mysterious mathematical properties such as commutativity, monotonicity and right-identity, and that consequently PBT is unfeasible for real-world scenarios.
It’s not at all like this.

Collateral Properties are more concrete than this, and they are often fun to find and implement. You can learn a lot about them from:

Essential is better than Collateral

I might be a voice outside the chorus, but I think Collateral Properties are a bit overrated — and often excessively feared.

Many PBT tutorials start with the infamous reversal of a list example. I’ve never being completely happy with the classical implementation, exactly because it is based on a Collateral Property. The idea is that reversing a list can be tested observing that reversing the reversal of a list gives back the original list:

[Property]
void invariant_of_reversal(ImmutableArray<string> xs) =>
    Assert.Equal(xs, (Reverse(Reverse(xs))));

This says nothing about what reversing a list is, about its essence. It tackles a side effect, a derived observation.
In fact, it passes for the following dishonest implementation without batting an eyelid:

IEnumerable<string> Reverse(IEnumerable<string> xs) => xs;

This sucks.

If you really wanted to capture the essence of revesing a list, you should start from the requirement:

Reversing a list is the action of changing 
the order of elements so that 
they appear in the opposite sequence:
the first element becomes the last element, 
the second element becomes the second-to-last element, 
and so on, until the last element 
becomes the first element.

Then you could try with a direct translation to an Essential Property. That would lead to something like:

[Property]
bool specification_of_reversal(List<string> xs)
{
    var reversed = Reverse(xs).ToList();

    for(var i = 0; i < xs.Count; i++)
    {
        if (xs[i] != reversed[xs.Count - i - 1])
            return false;
    }

    return true;
}

This easily spots the dishonest implementation. Hurray!

In the last part I show you how applying property testing affects the practice of TDD. Grab a fruit, bite it and let’s get started.

References

See References

Comments

GitHub Discussions