5 systematic ways of coming up with property-based tests

This is a cheat sheet based on a great talk "How to specify it! A guide to writing properties of pure functions" by John Hughes. This talk has a lot of information easy to forget so a cheat sheet may help you refreshing memories without watching the whole talk again.

If you didn't watch the talk yet – watch it. Otherwise, you won't understand much.

There are 5 systematic ways of formulating properties. The current example is a binary search tree.

1. Is there an invariant?

Every operation should return valid results.

If there is an invariant that your function must satisfy – you can write a test that checks this invariant.

Example: every operation returning a tree should return a valid tree.

You should also make such tests for your generators. And for your shrink functions.

Test results: 4 properties, 5/8 bugs missed. Average effectiveness of property – 38%. Still considered as required tests.

2. What is the postcondition?

After calling insert we should be able to find the key inserted, and any other keys present beforehand.

Test results: 5 properties, 0/8 bugs missed. Average effectiveness of property – 79%. Relatively slow in finding bugs.

3. Metamorphic properties

How does changing the input of insert change its result?

Metamorphic testing – running the code in the test twice on related arguments and checking that you get related results.

Example: If you're inserting two different values to the same tree – you can flip the insert order and results will be equivalent.

You can make similar tests for every pair of operations.

Test results: 16 properties, 0/8 bugs missed. Average effectiveness of property – 90%. Relatively slow in finding bugs.

4. Inductive properties

Properties that look like a definition of a function you're testing.

Examples:

union nil t === t – union of a tree t and an empty tree is the same as the tree t.
union (insert k v t) t' =~= insert k v (union t t') – insert a value into union of trees t and t' produces the same result as union of trees t and t' with value inserted into one of them.

Inductive properties are the properties that you write down and you can make an argument by induction that the only function that can pass these tests is the correct one.

5. Model-based properties

We define the mapping from our complex implementation into some much simpler data type. We call that mapping an abstraction function. We abstract the implementation to a model. And then we implement our operation on the model. … You get the same result both ways round.