Property-Based Testing · Lesson 01

Model the Resource, Not the Code

A CRUD resource is a Map with a complicated implementation. That makes it the easiest place to start with model-based testing. A command endpoint, like Figma's operations on a frame, looks similar but needs different properties. By the end you can write the harness for one CRUD resource and say which properties a command endpoint has.

Terms

Property

A statement that must hold for every generated input.

SUT

System under test. Here: the real repository or endpoint, with its database, ORM and caches.

Model

A much simpler implementation of what the SUT is supposed to do. fast-check: “not a carbon copy of the system but a simplified representation of it.”

Command

One generated operation. check(model) says whether it may run now; run(model, real) applies it to both and asserts they agree.

Shrinking

After a failure, the tool removes steps and simplifies values until it has the shortest sequence that still fails.

Metamorphic

A property that relates two calls instead of predicting one. Change the input in a known way, and the output must change in a known way. Hughes: “Related calls return related results.” Example: adding a filter must return a subset. Lesson 02 covers it in depth.

Oracle

Whatever tells the test the right answer. In model-based testing, the model is the oracle.

Why a CRUD resource is a good fit

Goldstein et al. interviewed 30 engineers at Jane Street who use PBT daily. The most common kind of property, used by 17 of 30, was differential or model-based: compare the code to a simpler reference. One participant summarised when PBT is worth it:

“[PBT is] most useful when… you have a really good abstraction with a complicated implementation.”

A soft-deletable resource with a unique slug fits this exactly. The abstraction fits in a few lines: a map from id to fields, a deletedAt per entry, and one rule about slugs. The implementation is a SQL table, a partial unique index, an ORM, a cache and a serialiser. All the bugs live in the implementation.

The harness for one resource

type Row = { slug: string; name: string; deletedAt: Date | null };
type Model = { rows: Map<string, Row>; ids: string[] };   // ids in creation order

const live = (m: Model) => [...m.rows.entries()].filter(([, r]) => !r.deletedAt);
const slugTaken = (m: Model, slug: string) => live(m).some(([, r]) => r.slug === slug);

// A target is usually a row the model has seen (deleted ones included), sometimes an id that never existed.
type Target = { existing: number } | { unknown: string };
const target = fc.oneof(
  { weight: 9, arbitrary: fc.nat().map((existing) => ({ existing })) },
  { weight: 1, arbitrary: fc.uuid().map((unknown) => ({ unknown })) },
);
const NEVER_CREATED = '00000000-0000-4000-8000-000000000000';
const resolve = (m: Model, t: Target) => {
  const id = 'unknown' in t ? t.unknown
           : m.ids.length ? m.ids[t.existing % m.ids.length] : NEVER_CREATED;
  return { id, row: m.rows.get(id) };          // row undefined → expect notFound
};

class Create implements fc.AsyncCommand<Model, ProjectApi> {
  constructor(readonly input: { slug: string; name: string }) {}
  check = () => true;
  async run(m: Model, api: ProjectApi) {
    const res = await api.create(this.input);
    if (slugTaken(m, this.input.slug)) return assert.equal(res.kind, 'conflict');
    assert.equal(res.kind, 'ok');
    m.rows.set(res.id, { ...this.input, deletedAt: null });
    m.ids.push(res.id);
  }
  toString = () => `create(${this.input.slug})`;
}

class Delete implements fc.AsyncCommand<Model, ProjectApi> {
  constructor(readonly t: Target) {}
  check = () => true;
  async run(m: Model, api: ProjectApi) {
    const { id, row } = resolve(m, this.t);
    const res = await api.delete(id);
    if (!row || row.deletedAt) return assert.equal(res.kind, 'notFound');
    assert.equal(res.kind, 'ok');
    row.deletedAt = new Date();
  }
  toString = () => `delete(${JSON.stringify(this.t)})`;
}

class List implements fc.AsyncCommand<Model, ProjectApi> {
  check = () => true;
  async run(m: Model, api: ProjectApi) {
    const res = await api.list();
    assert.deepEqual(res.map((p) => p.id).sort(), live(m).map(([id]) => id).sort());
  }
  toString = () => 'list';
}
// + Get, Patch, Restore — same shape

const slug = fc.constantFrom('a', 'b', 'A');   // few values → collisions are common
const commands = [
  fc.record({ slug, name: fc.string() }).map((x) => new Create(x)),
  target.map((t) => new Delete(t)),
  fc.constant(new List()),
];

test('projects behave like the model', () =>
  fc.assert(fc.asyncProperty(fc.commands(commands), (cmds) =>
    fc.asyncModelRun(async () => {
      await resetDb();
      return { model: { rows: new Map(), ids: [] }, real: new ProjectApi(db) };
    }, cmds)), { numRuns: 50 }));

There are three design choices in this code. Each one is easy to get wrong:

1. The slug generator draws from three values. With fc.string(), two random slugs would almost never be equal, and the conflict path would never run. Narrow generators make the interesting cases common. 'A' is there to test your case-sensitivity rule.
2. Delete takes a Target, not an id. Nine times in ten it is an index that resolve turns into a row the model has seen, including deleted ones. That is how delete → delete gets generated. One time in ten it is a random UUID that never existed, which covers the plain 404 path. A fully random id would almost never hit a real row.
3. The model never calls your service code. Every expected result comes from the Map. If the model calls the code under test, it can only ever agree with it.

Known failures go in front of the random runs as fixed sequences. asyncModelRun accepts any list of commands:

test('regression: restore into a taken slug', () =>
  fc.asyncModelRun(setup, [new Create({ slug: 'a', name: '' }), new Delete({ existing: 0 }),
                           new Create({ slug: 'a', name: '' }), new Restore({ existing: 0 })]));

The contrast: a command endpoint

Now a different kind of endpoint. A design editor, in the style of Figma, has one endpoint per document:

POST /frames/:frameId/commands
{ "mutationId": "c1-42", "type": "reparent", "node": "rect-7", "newParent": "group-2", "index": 0 }
{ "mutationId": "c1-43", "type": "move",     "node": "group-2", "dx": 10, "dy": 0 }
{ "mutationId": "c1-44", "type": "delete",   "node": "group-2" }   // deletes the subtree

In Data Synchronisation 01, this was a mutator receiving mutations. Here the question is what to test.

The difference from CRUD is where the complexity is. In the CRUD resource the intended behaviour is simple and the storage is complicated. In the command endpoint the intended behaviour is the complicated part. A reparent has to keep the tree acyclic, update indices among siblings and convert child coordinates into the new parent's space. A model that predicts the exact result of every reparent would be a second implementation of the editor. That is the case fast-check warns about: the test compares the code with a copy of itself.

So for command endpoints you stop predicting the exact result and check relations instead. These are Wlaschin's patterns, and none of them needs to know the right answer:

The harness itself works the same way for both. A command endpoint still gets random command sequences and shrinking. The difference is in run: it asserts invariants and relations instead of comparing against a predicted value.

class Reparent implements fc.AsyncCommand<Model, FrameApi> {
  constructor(readonly node: Target, readonly parent: Target) {}
  check = () => true;
  async run(m: Model, api: FrameApi) {
    const [n, p] = [resolve(m, this.node).id, resolve(m, this.parent).id];
    const before = await api.document();
    const res = await api.command({ type: 'reparent', node: n, newParent: p, index: 0 });
    const after = await api.document();
    assertTreeInvariants(after);                              // acyclic, one parent each, ids unique
    if (res.kind === 'rejected') assert.deepEqual(after, before);   // rejection changes nothing
    else assert.equal(parentOf(after, n), p);                 // postcondition, not a full prediction
  }
}

The reparent assertion is weaker than a full prediction. It doesn't say where the node ends up in coordinates. It does catch the bugs that matter most, though: cycles, lost nodes and partial writes. Hughes calls a check like the last line a postcondition: a relation between a single call's arguments and its result.

Property failed after 31 runs, shrunk 14 times
Counterexample: [reparent(#1 → #0), reparent(#0 → #1)]
AssertionError: assertTreeInvariants: cycle detected (group-1 → group-0 → group-1)