Property-Based Testing · Lesson 03

Five Ways to Specify It

Wlaschin's seven patterns help you find properties. Hughes's five approaches tell you how much each kind of property is worth. He wrote all five for one data structure, planted eight bugs, and counted which properties caught them. By the end you can choose the approach for a function and predict how strong the result will be.

The paper is John Hughes, How to Specify It! A Guide to Writing Properties of Pure Functions (TFP 2019, LNCS 2020). Hughes co-invented QuickCheck, the first PBT tool. His running example is a binary search tree used as a key–value map, with insert, delete, union and find. Below, each approach is shown first in his terms and then translated to CRUD code. The translations are mine; the paper covers pure functions only.

1 · Validity

“Every operation should return valid results.”

Write a function valid(x) that checks the data's invariant, and assert it on the output of every operation. For the tree: keys in the left subtree are smaller, keys in the right are larger. For a CRUD entity: dueDate ≥ issueDate, total = Σ lines, every child's tenant equals its parent's.

Hughes's second slogan in this section is “Test your tests.” His tree generator had a bug that produced invalid trees, and then delete and union “failed” even though they were correct, because they had been given invalid input. The fix is a property about the generator itself:

test('the invoice generator only produces valid invoices', () =>
  fc.assert(fc.property(invoiceArb, (inv) => assert.ok(valid(inv)))));

If this fails, fix the generator before looking at any other failure. This is your Q2 answer in its strongest form: don't only make invalid inputs rare, test that the generator does what you think.

How strong: weak. Validity properties missed 5 of the 8 bugs. An insert that deletes instead, or a union that computes a set difference, still returns a valid tree. Your Q4 answer “total ≥ 0” has the same weakness: an applyDiscount that always returns 0 passes it.

2 · Postcondition

“Postconditions relate return values to arguments of a single call.”

Ask: “what should be true after calling f?” After insert(k, v, t), find(k) returns v, and every other key returns what it returned before. For CRUD: after PATCH {name}, GET returns the new name and the old values of every other field.

When the postcondition is hard to state, Hughes's trick is to construct a test case whose outcome is easy to predict. You can't easily say what find(k, t) should return for a random tree, but you can for find(k, insert(k, v, t)): it's v. In CRUD terms: you can't say what GET /projects/:id returns for a random id, but you can for an id you just created.

How strong: every bug was caught by at least one postcondition, but slowly: an average of 77 tests to fail (range 7–245). The reason is below.

3 · Metamorphic

“Related calls return related results.”

Lesson 02 in full. Two things Hughes adds:

• The first version is usually wrong, in a useful way. “Insertion order doesn't matter” failed immediately with two inserts of the same key. The property had found an unstated rule: the last insert wins.
• You need two kinds of equality. After the fix it still failed: the two trees held the same data in different shapes. Hughes defines equivalence (same contents, compared via toList) next to structural equality. In CRUD the same problem shows up as responses that differ only in ids, timestamps or array order. Decide which fields are part of the contents before comparing.

How strong: individually uneven, but strong together. Some caught a bug in 2.4 tests on average, others needed 714. The weak variants, which used a precondition to exclude the tricky case (e.g. “only when the two keys differ”), missed bugs that the full versions caught.

4 · Inductive

“Inductive proofs inspire inductive tests.”

Relate a call to a call on a smaller argument, and cover the base case. Hughes's two properties for union:

union(nil, t)                ≡  t                          // base case
union(insert(k, v, t), t2)   ≡  insert(k, v, union(t, t2))  // step: one smaller first argument

Together these fully specify union, on one condition: every tree must be buildable from insert alone. Hughes tests that condition as a property of its own. This is Wlaschin's “solve a smaller problem first”.

CRUD code has more of these than you'd expect, wherever something is computed over a collection:

revenue([])              === 0
revenue([...invs, inv])  === revenue(invs) + inv.totalCents

bulkCreate([])           →  no change
bulkCreate([...xs, x])   ≡  bulkCreate(xs); create(x)

How strong: complete when the cases cover everything, but only for operations that are built up step by step. Most CRUD endpoints aren't.

5 · Model-based

“Abstract away from details to simplify properties.”

This comes from Hoare (1972). Choose an abstraction function from the real data to a simple model. For the tree it is toList, a sorted list of pairs. Then check that running the real operation and abstracting gives the same result as abstracting first and running a simple version of the operation:

toList(insert(k, v, t))  ===  sortedInsert([k, v], toList(t).filter(([key]) => key !== k))

Lesson 01 is the same idea with state: the abstraction function maps your database to a Map.

How strong: the strongest. One property per operation found every bug in that operation, in 5.8 tests on average (range 3.1–9.8).

Why the model was fastest

The postcondition and the model-based property for union are logically equivalent, yet one needed 50 tests to find a bug and the other 8.4. The postcondition checks one random key of the result. The model-based property compares every key and value. A test can hit the bug without the postcondition noticing, because it checked the wrong key. How much of the output a property checks matters as much as what it checks.

Hughes's own conclusion:

“If time is limited, then writing model-based properties may offer the best return on investment, in combination with validity properties to ensure we don't encounter confusing failures caused by invalid data. In situations where the model is complex (and thus expensive) to define, or where the model resembles the implementation so closely that the same bugs are likely in each, then metamorphic properties offer an effective alternative, at the cost of writing many more properties.”

This is the same rule as lessons 01 and 02, now with numbers. Note the scale: one data structure and eight bugs that Hughes planted himself. It shows the relative strength of the approaches clearly, but it is not a survey of real bugs.

One note on generators

Hughes measured his test data and found that in about 80% of tests the key being looked up wasn't in the tree at all, so most of the effort went into the boring case. Drawing keys from a smaller range raised “present” to 55%. This is why lesson 01's slugs come from three values. Use fc.statistics to see the distribution your generator actually produces.