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

insertwe should be able tofindthe 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

inputofinsertchange itsresult?

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 theimplementationto amodel. And then we implement our operation on the model. … You get the same result both ways round.

We're using the *model* as a reference implementation.

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

Tweet with original paper: https://twitter.com/rjmh/status/1146789597235613697