What Is a Property?

When talking about Property-Based Testing, we typically talk in very abstract terms. There are properties, which define the correctness; there are generators, which define the domain; the PBT framework gives us APIs for writing property-based tests that combine the properties with the generators to find bugs. It's all very nice and simple.

A (surprisingly) large chunk of my time goes into exploring different PBT frameworks, many times porting an existing PBT workload to use a new one instead of the other. This requires me to build abstractions on what a PBT framework is, which should have been very easy if the simple definition I gave in the first paragraph captured what PBT is. Unfortunately it doesn't, so let's see what the issue is. A property is a universally quantified computation that must hold for all possible inputs. The simplest model of a property in a programming language is a function that returns a boolean, such as the one below:

For instance, \l -> reverse (reverse l) == l is a property, it asserts double reversion leads to the original list. This gets slightly complicated with preconditions, which are rules that state if an input is valid or not. So we can write things like:

data Database = ...
(==>) precondition property =
if precondition then Just property else Nothing
=
let insert = Insert table values
select = Select table "*"
in
hasTable db table ==> (values `elem` query (execute db insert) select)

Where ==> is the implication operator, which states that if the precondition (the left-hand side) is not satisfied, then the property cannot be tested. In our case, the precondition is hasTable db table, which checks if the database has the specified table. If it doesn't, then we don't care about the result, we just discard it. If the database has the table, then we execute the insert and check if the select query returns the values we inserted.

Now that we have a property at hand, we need some random generators for it. We can write Arbitrary instances for all the input types and let QuickCheck handle the rest.

data Value = Number Int | String String | ...
arbitrary = oneof [Number <$> arbitrary, String <$> arbitrary, ...]

Well, not really. When we write these instances, what do you think QuickCheck does? It generates a random database, a random string, a list of random Values, and then runs the prop_insert_select function. In what percent of cases do you think a random string is a valid table name that exists in the database?

What we want is a dependent generator, where some values can depend on the others:

genValidInput = do
-- Decide how many tables we want to create
numTables <- choose (1, 10)
-- Randomly generate the tables
tables <- vectorOf numTables genTable
-- Create an empty database
let db0 = emptyDatabase
-- Populate the database with the generated tables
let db = foldl createTable db0 tables
-- Now we can generate a valid table name and values
let tableNames = map tableName tables
table <- elements tableNames
values <- genValuesFor db table
return (db, table, values)

Now we don't need to worry about the precondition failure because the inputs are valid by construction. The table is selected from the already existing list of tables in the database, so it will never fail.

This highlights that the generator is not independent from the property. To be fair, that is a common requirement, you cannot just randomly sample data in the hopes of running into interesting inputs, you need to be aware of the system under test.

QuickCheck already has support for this style of property-based test writing without making you write your property under Gen using the forAll combinator:

prop_insert_select =
forAll arbitrary $ \db ->
forAll arbitrary $ \table ->
hasTable db table ==>
forAll arbitrary $ \values ->
let insert = Insert table values
select = Select table "*"
in
values `elem` query (execute db insert) select

In this style, every forAll combinator takes a generator and produces a context with access to the generated value. The Hypothesis intro puts it especially well from a practical perspective: you write tests which should pass for all inputs in whatever range you describe, and let Hypothesis randomly choose which of those inputs to check. Essentially, Property-Based Tests leverage properties as universally quantified statements, but many times, they cannot use them without breaking the abstraction boundaries.