functional-programming-snake/course/12-property-testing.md

Module 12 — Testing with properties (bonus)

Time: ~4 h · You'll edit: JS js/src/check.js · Scala scala/src/Check.scala · F# fsharp/src/Check.fs Tests: JS cd js && node --test "test/m12-*.test.js" · Scala cd scala && ./test.sh M12 · F# cd fsharp && ./test.sh M12 Prerequisites: Modules 1–5 and Module 10, including the turn queue of Exercise 10.6 (you need Random, update, history, the Frame action and queued). Modules 6–9 and 11 are not needed.

Why this module

Every test you have run in this course is an example: this state, this action, this expected state. Examples are precise, and they are easy to read. They also have one weakness, which Puzzle 3 of Module 10 showed: an example checks a case that somebody thought of. The first version of this course's speed-up rule had six fixture cases, all green, and still made the snake jump two cells in 25 ms after every third apple. Nobody had written the case "the score changes on this very frame", because nobody had thought of it. That is the kind of bug you are least likely to write an example for.

A property is a different kind of test. Instead of one input and its expected output, you state something that must be true for every input:

• every state of every game has the snake on the board;
• the snake never overlaps itself;
• the time between two moves is always movesEvery(score) frames.

Then you let the computer look for an input that breaks the statement, by trying hundreds of random ones. If it finds one, it hands you a counterexample.

Random tests have a bad reputation: they fail on Tuesday, pass on Wednesday, and nobody can reproduce the failure. That reputation comes from hidden randomness. You solved that problem in Module 4. A random test input is a value drawn from a Random<A> with a seed, so a failing test is reproduced by one number. And because the game is a fold over a list of actions (Module 5), a counterexample is a replay: a list you can run again, print, and cut down to the two key presses that matter.

In this module you build a small property-testing library from the parts you already have, about forty lines of code. Then you point it at deliberately broken versions of the game and watch it find each bug and reduce it to its essence. At the end you generate whole game states instead of games, and catch a bug that no statement about a single state can see, by comparing two implementations of the same rule.

Learning objectives

After this module you can:

• distinguish an example-based test from a property, and state properties of several kinds (invariants, relations between runs, laws);
• implement generators of test data as Random values (elementOf, listOf) and recognise listOf as the same pattern as sequence from Module 7;
• implement a pure test runner forAll that returns a report with the counterexample and the seed that reproduces it;
• implement shrinking for lists (removals, minimize) and explain what "1-minimal" means and why total rules make shrinking easy;
• write an invariant checker for the game state and explain how it relates to "making illegal states unrepresentable";
• judge whether a property can detect anything at all, using deliberately broken implementations (mutants);
• implement a generator of structured data whose parts depend on each other (genSnake), and explain why the order of the draws is part of its contract;
• use a second, independently written implementation as a test oracle (advanceSpec), and explain which bugs it can and cannot find.

Concepts

1. From examples to properties

Take dropLast from Module 1. An example test says:

dropLast([1, 2, 3])  is  [1, 2]

A property says something about every list xs:

for every list xs:   dropLast(xs) has length max(0, length(xs) - 1)
for every list xs:   dropLast(xs) is the beginning of xs

Neither property mentions a particular list, and together they pin dropLast down completely. To check a property you need three things: a way to produce many inputs, a way to run the check on each of them and report what happened, and, when it fails, a way to make the failing input small enough to understand. Those are the three parts of this module: generators, forAll and shrinking.

From everyday programming: you may know fuzzing: throwing large amounts of random input at a parser or a network service to see whether it crashes. A property test is a fuzzer with an opinion. It does not only ask "did it crash?" but "is this statement about the result still true?", and it runs in milliseconds as part of the unit tests.

2. A generator is a Random

What is "a way to produce test inputs"? A function from a seed to a value and a new seed, so that the next input can be drawn from where the previous one stopped. You built exactly that type in Module 4:

Random<A>  =  seed -> [A, seed]

So there is no new type in this module. A generator of numbers below 10 is intBelow(10). Two small combinators give you everything else the game needs:

• elementOf(xs) picks one element of a non-empty list: draw an index with intBelow(length) and look it up. That is a map.
• listOf(gen, n) draws n values from gen, one after another, and collects them in a list. The first draw uses the incoming seed, the second draw the seed the first one left behind, and so on.

listOf is worth a second look. "Run these computations one after another and collect the results" is what sequence did for IO in Module 7, and it is built the same way: from flatMap and pure, by recursion.

listOf(gen, 0)  =  pure([])
listOf(gen, n)  =  flatMap(gen, a => map(listOf(gen, n - 1), rest => [a, ...rest]))

Read the second line as: draw one value a; then draw the remaining n - 1 values as a list rest; the result is a in front of rest. Nowhere do you see a seed. flatMap threads it, which is the reason you wrote flatMap in the first place.

With these two, a generator of random games is one line, and it is given in your stub:

genActions(n) = listOf(elementOf([Tick, Tick, Tick, Turn Up, Turn Down, Turn Left, Turn Right]), n)

Tick appears three times in the list, so about three actions in seven are ticks. Repeating an element is the simplest way to make it more likely.

Language note. JS: listOf(gen, n), data first. Scala: Check.listOf(gen, n). F#: Check.listOf n gen, data last, so that it reads gen |> Check.listOf 40.

3. forAll: a test runner that is a pure function

forAll(gen, prop, runs, seed) draws runs values from gen, starting from seed, and calls the property prop (a function from a value to a boolean) on each. It stops at the first value for which prop is false.

Most test frameworks report a failure by throwing an exception or printing to the console. Ours returns a value:

all runs passed:   Passed(runs)
a run failed:      Failed(run, seed, value)

• run is the number of the failing draw, counted from 0;
• value is the counterexample;
• seed is the seed that draw started from, so drawing from gen with seed gives value again.

In JS the report is a plain object, { ok: true, runs } or { ok: false, run, seed, value }. In Scala and F# it is a small sum type, CheckResult, given in your stub.

forAll has no loop counter and no "current seed" variable. It is a recursion that carries the run number and the seed as arguments, the same way interval carried last in Module 8.

Because forAll is pure, the test of a test runner is an ordinary equality: the same generator, property, number of runs and seed give the same report, every time, on every machine. A failure in one track's test suite can be reproduced in another track with the same seed, because all three tracks draw the same numbers (Module 4).

From everyday programming: a flaky test is a test whose result depends on something it does not control: the clock, the order of a hash map, a random number. The usual cure is to hunt down each hidden input and pin it. Here there is nothing to hunt down. The only source of variation is the seed, and the seed is an argument.

4. Shrinking: from forty actions to two

Suppose forAll reports that this list of 40 random actions breaks a property:

Tick, Turn Down, Tick, Tick, Turn Right, Turn Up, Tick, Turn Left, Tick, Tick, Turn Up, Tick, ... (28 more)

Somewhere in there is a bug, but which of the 40 actions matter? The idea of shrinking is to let the computer find out: try smaller inputs, and keep any that still fails.

For a list, the simplest "smaller input" is the list with one element removed:

removals([a, b, c])  =  [[b, c], [a, c], [a, b]]

minimize(xs, fails) repeats one step: look through removals(xs) for the first list that still fails. If there is one, continue from it. If there is none, stop and return xs.

The result is called 1-minimal: it fails, and removing any single element makes it pass. Every element of it is needed. It is not always the smallest failing list that exists. Take the (artificial) failure "the list has exactly one or exactly three elements": minimize stops at three elements, because every list of two passes, although a list of one would fail too. For bugs in real programs, 1-minimal is almost always good enough, and it is cheap: at most n rounds of at most n tries.

Why is this so easy for our game? Because of two decisions made long ago:

• A game is a list of actions (Module 5). The test input is plain data, so "a smaller input" has an obvious meaning.
• The rules are total (Module 3). Every list of actions is a valid game. If turn threw an exception for an illegal turn, most of the shortened lists would crash for reasons that have nothing to do with the bug, and the shrinker would be led astray. Because "does not apply" means "unchanged", you can delete any action from any game and still have a game.

From everyday programming: this is what you do by hand with a bug report. A user sends twenty steps to reproduce a crash; you leave out a step, try again, and keep going until every remaining step is needed. git bisect automates the same search over a list of commits. The technique has a name, delta debugging, and minimize is its simplest form.

5. What to check: invariants

The most useful properties of a program with state are its invariants: statements that hold for every state the program can ever reach.

Module 2 was honest about the model: the types rule out some nonsense (a status that is paused and over), but a GameState can still be built with a snake outside the board, an apple inside the snake, or a snake whose cells are scattered across the board. Types could not exclude those states, at least not conveniently. The rules are supposed to: starting from newGame(seed), no sequence of actions should ever produce one.

An invariant checker turns that claim into a function:

violations(state)  =  the names of the invariants this state breaks   (an empty list: the state is sane)

Name	The state is sane when...
snake-not-empty	the snake has at least one cell
snake-in-bounds	every cell of the snake is on the board
snake-no-overlap	no two cells of the snake are equal
snake-connected	each cell of the snake is exactly one step (up, down, left or right) from the one before it
apple-in-bounds	the apple, if there is one, is on the board
apple-not-on-snake	the apple, if there is one, is not on a cell of the snake
turn-not-reversed	nextDir is not the opposite of dir
queued-not-reversed	queued is none, or is not the opposite of nextDir (the turn queue of Module 10)

violations returns the names in this order. It returns names and not a single boolean, so that a failing test says what is wrong. Each row is one small predicate; the function is a filter over a table of (name, predicate) pairs.

The property is then one line:

for every list of 40 random actions:   every state in history(newGame(1), actions) has no violations

Think of invariants as the part of "make illegal states unrepresentable" that the type system left over. Where a type can exclude a bad state, use the type: the compiler checks it for all programs, for free. Where it cannot, write the invariant down as a function and check it on thousands of random games.

6. What to check: relations and laws

Invariants look at one state at a time. Some requirements are about how states relate to each other.

A relation between moments of one run. "Every step of the snake lasts exactly movesEvery(score) frames" is a statement about a whole history. To check it, you need the gaps between consecutive moves:

moveGaps(states)  =  the distances between the positions in the list where the head moved

The snake "moves at index i" when the head of states[i] differs from the head of states[i - 1]. If it moves at indices 2, 5 and 12, the gaps are [3, 7]. With moveGaps the requirement of Module 10 becomes checkable, and the tests of this module run it against the tempting rule of Puzzle 3.

Laws. Some equations hold between whole computations, for example the replay law of Module 5:

replay(s, a ++ b)  ==  replay(replay(s, a), b)

Here is a question that separates a useful property from a useless one: could this property ever fail? Look at the replay law again. It follows from the definition of a fold, for any step function whatsoever. A game in which the snake teleports, an update that ignores every action, a version full of bugs: all of them satisfy it. So a test of this law tests replay (is it really a left fold?) and tells you nothing about the game.

There is a practical way to answer "could it fail?": break the program on purpose and see whether the property notices. A deliberately broken copy is called a mutant, and a mutant that fails a test is said to be killed. The last tests of this module do exactly that, with these mutants:

Mutant	The bug	Caught by
turn checks against nextDir	Puzzle 2 of Module 3: the quick double turn	turn-not-reversed
advance forgets the walls	the snake walks off the board	snake-in-bounds
Tick forgets the turn queue	Exercise 10.6 done in Frame but not in Tick	queued-not-reversed
the queue accepts a reversal	Exercise 10.6 without the "not the opposite of nextDir" check	queued-not-reversed
the tempting frame rule	Puzzle 3 of Module 10: steps of uneven length	the gaps of moveGaps
advance checks the old snake	Puzzle 1 of Module 3: death by the tail that is moving away	comparison with advanceSpec (section 8)

For the first four, the tests also shrink the counterexample, and the results are worth predicting. What is the shortest list of actions that makes a snake reverse into itself if turn checks the wrong direction? What is the shortest list that walks the snake of newGame(1) off a board without walls? (The head starts at x = 10 on a board 20 wide, heading Right.) Decide before you run the tests; the test titles give the answers.

7. Generating states, not only games

Every test input so far has been a list of actions, played from newGame. That only reaches the states that random play reaches, and random play is a poor explorer: the snake grows only when it eats, and forty random actions rarely eat more than one apple. A long snake coiled up so that its head is right next to its own tail, the situation of Puzzle 1, practically never happens.

When the function under test takes one state, as advance does, you can skip the game and generate the state directly. The difficulty is that the parts of a state depend on each other. The snake's cells must be neighbours and must not repeat; dir must agree with the first two cells; the apple must be on a free cell. A generator that drew each field independently would produce almost nothing but nonsense, and a test of advance on nonsense says nothing about the game.

The way out is to draw the parts in the order in which they depend on each other, each draw using what the earlier ones produced. That is exactly what flatMap does: the next generator is chosen from the value of the previous one. For the snake:

genSnake(width, height, maxLen):
  draw the head: x with intBelow(width), then y with intBelow(height)
  then, until the snake has maxLen cells:
    the candidates are the neighbours of the LAST cell, in the order Up, Down, Left, Right,
    that are on the board and not yet in the snake
    if there are none, stop early; otherwise append elementOf(candidates) and go on

From seed 0 on a 5 x 5 board with maxLen 6, the head is (3,2) and the walk continues up and then left along the top row:

        x=0  x=1  x=2  x=3  x=4
  y=0    5    4    3    2    .        snake (head first): (3,2) (3,1) (3,0) (2,0) (1,0) (0,0)
  y=1    .    .    .    1    .        the numbers give the order in which the cells were drawn
  y=2    .    .    .    H    .
  y=3    .    .    .    .    .
  y=4    .    .    .    .    .

The order of the draws, and the order Up, Down, Left, Right of the candidates, are part of genSnake's contract, written in the stub. They decide which snake a seed gives. Because all three tracks follow them, a counterexample found from a seed in one track is the same counterexample in the others.

genState(width, height) is given in your stub and builds on genSnake: a length limit between 1 and width * height, a snake, dir read off the first two cells (Right for a one-cell snake), nextDir equal to dir or a perpendicular direction, an apple on a random free cell or none, and nothing queued. Read it: it is four flatMaps, each one choosing the next generator from what came before.

A generator is code, and code has bugs. If genState produced a disconnected snake, every later test would complain about states the game can never reach, and you would hunt for bugs that are not there. So the first test of a generator is a property of the generator: every generated state is sane: 500 states of a 5x5 board have no violations.

From everyday programming: test-data builders and factories (a UserFactory that fills in a valid email, a hashed password and a creation date before an account object is saved) solve the same problem: produce objects whose fields satisfy the constraints between them, so that the test can concentrate on what it wants to check. A property-testing generator is a factory that picks random valid objects, and can therefore find the valid object nobody thought of.

8. A second implementation as an oracle

Generated states make it possible to test advance on hundreds of coiled-up snakes. But test it against what? Invariants say whether a state is sane, and the bug of Puzzle 1 produces only sane states: it ends the game one step too early, and a finished game is a perfectly valid state. To catch a result that is valid but wrong, you need to know the right result. Something that knows it is called a test oracle.

For one hand-written example, the oracle is you: you write the expected state into a fixture. For 500 random states, you need a program. The usual answer is a second implementation, written independently, and the property

for every generated state s:   advance(s) == advanceSpec(s)

The second implementation is only useful if it does not share the first one's mistakes, so it should be written in a different way. Module 3's advance decides about the new head: compute the body that remains, then ask whether the head lands on the board and outside that body. advanceSpec decides about the resulting snake: build the whole snake the step would produce (the new head in front, then the old snake without its last cell unless eating), and ask violations, the checker you wrote in Exercise 12.4, whether that snake is on the board and free of overlap. If it is not, the step is deadly, and the result is Module 3's game over. It is the rule stated as a requirement on the outcome: "after a step, the snake must still be a legal snake".

Now look at the wrong check of Puzzle 1 again: "the new head must not be on the old snake". It is a statement about the old snake, and it disagrees with "the new snake must not overlap" exactly when the head moves onto the cell the tail is leaving. The comparison test finds such a state in the 22nd draw (run 21) from seed 2024:

        x=0  x=1  x=2  x=3  x=4
  y=0    1    2    .    .    .        snake (head first): (0,1) (0,0) (1,0) (1,1) (1,2) (1,3) (0,3) (0,2)
  y=1    H    3    .    .    .        heading Down; the head's next cell (0,2) is the tail T
  y=2    T    4    .    .    .        A is the apple
  y=3    6    5    A    .    .
  y=4    .    .    .    .    .

The wrong check says "game over"; advanceSpec says the snake moves on, its tail having left (0,2) at the same moment. No invariant could have said which one is right, and the test no invariant sees the wrong collision check of Puzzle 1: every state it produces is sane shows that, too.

Two caveats. An oracle written by the same person on the same afternoon can share a misunderstanding of the rules with the code it checks; then the two agree and are both wrong. That is what the example fixtures, written from the specification, are for: advanceSpec must also pass Module 3's twelve advance cases. And an oracle has to be simpler or more obviously right than the code it checks, or you have only doubled the code you must trust. advanceSpec is simpler in one sense: it delegates the whole question "is this a legal snake?" to a function that was already tested on its own.

From everyday programming: this is differential testing. When a team rewrites a slow service, they often run the old and the new version side by side on the same requests and compare the answers before switching. Compiler writers generate random programs and compare the output of two compilers. A refactoring is safe to the extent that the code after it agrees with the code before it, and keeping the old version around as an oracle turns that into a test.

9. What random testing does not find

Be as honest about this tool as Module 2 was about the model.

• A property only sees what it states. The invariants of section 5 cannot see the wrong collision check of Puzzle 1: it ends the game too early, and a game that has ended is still a sane state. Catching it took a different kind of property, the comparison with a second implementation of section 8. That one has its own blind spot: it cannot see a mistake that both implementations make.
• Random inputs reach the likely states. Forty random actions from a new game almost never eat three apples. So random play from newGame would practically never reach the first speed-up, and would not find the bug of Puzzle 3. The tests therefore start from a hand-made state: a long corridor with the third apple right in front of the head, and a random number of frames already counted. Generating states directly (section 7) is the other answer. Choosing where to start and what to generate is the real craft of property testing.
• Passing is evidence, not proof. 300 random games that keep every invariant make a bug less likely. They do not show that there is none. A proof needs reasoning (as in question 3 of Module 5) or a tool that explores every reachable state.

Exercises

About test names. The test titles quoted under "Tests" are the JavaScript ones; the JS runner prints them with the module in front (m12 listOf threads the seed from each draw to the next). The Scala and F# suites test the same things one-to-one, in each track's vocabulary (Passed/Failed instead of ok). Failing tests are reported by name when you run the module's tests; to read all titles, open scala/test/M12Check.test.scala or fsharp/tests/M12Check.fs. Fixture-based tests have the same case names in every track.

All functions are pure: no loops, no reassignment, no mutation. The purity audit checks this file like every other.

Exercise 12.1 — elementOf and listOf

JavaScript

export const elementOf = (xs) => ...          // Random<A>, for a non-empty array xs
export const listOf = (gen, n) => ...         // Random<A[]>

Scala

def elementOf[A](xs: List[A]): Random[A]
def listOf[A](gen: Random[A], n: Int): Random[List[A]]

F#

let elementOf (xs: 'a list) : Random<'a>
let listOf (n: int) (gen: Random<'a>) : Random<'a list>

Tests: elementOf picks the element at the index drawn by intBelow, elementOf of a one-element array always gives that element, and still uses up a draw, listOf(gen, 0) is the empty list and leaves the seed alone, listOf threads the seed from each draw to the next, listOf of a constant generator repeats the value and leaves the seed alone, genActions(n) gives n actions, the same ones for the same seed.

Watch out: write both with map, flatMap and pure from Module 4. If you find yourself unpacking a [value, seed] pair, you are doing by hand what flatMap does for you.

Exercise 12.2 — forAll

JavaScript

export const forAll = (gen, prop, runs, seed) => ...
// { ok: true, runs }  or  { ok: false, run, seed, value }

Scala

enum CheckResult[+A]:                 // given
  case Passed(runs: Int)
  case Failed(run: Int, seed: Long, value: A)

def forAll[A](gen: Random[A], runs: Int, seed: Long)(prop: A => Boolean): CheckResult[A]

F#

type CheckResult<'a> =                // given
    | Passed of runs: int
    | Failed of run: int * seed: uint32 * value: 'a

let forAll (runs: int) (seed: uint32) (prop: 'a -> bool) (gen: Random<'a>) : CheckResult<'a>

Tests: forAll reports success with the number of runs, forAll with zero runs succeeds without drawing anything, forAll reports the first failing draw, its value and the seed it started from, forAll stops at the first failure: the property is not asked about later values, forAll is reproducible: same generator, property, runs and seed give the same report.

Watch out: the seed in a failure report is the seed the failing draw started from, not the one it left behind. And each draw must continue from the previous draw's leftover seed; if every draw starts from the same seed, you test the same value runs times.

Exercise 12.3 — removals and minimize

JavaScript

export const removals = (xs) => ...           // removals([1, 2, 3]) -> [[2, 3], [1, 3], [1, 2]]
export const minimize = (xs, fails) => ...    // fails: list -> boolean, and fails(xs) is true

Scala

def removals[A](xs: List[A]): List[List[A]]
def minimize[A](xs: List[A])(fails: List[A] => Boolean): List[A]

F#

let removals (xs: 'a list) : 'a list list
let minimize (fails: 'a list -> bool) (xs: 'a list) : 'a list

Tests: removals lists every way to drop one element, in order, removals of an empty list is empty, and of a single element is one empty list, minimize keeps exactly the elements the failure needs, minimize keeps the order and the duplicates the failure needs, minimize of a list that fails whatever you remove is the empty list, minimize returns a list that still fails and has no failing removal (1-minimal).

Watch out: continue with the first failing removal, in the order of removals. The tracks must agree on which minimal list they report.

Exercise 12.4 — violations

JavaScript

export const violations = (state) => ...      // string[], in the order of the table in section 5

Scala

def violations(state: GameState): List[String]

F#

let violations (state: GameState) : string list

Fixture: fixtures/m12-violations.json, 21 cases: six sane states (a-sane-state-has-no-violations, no-apple-is-fine, a-one-cell-snake-is-fine, a-queued-turn-is-fine, ...), one or two cases per invariant (head-off-the-right-edge, snake-with-a-diagonal-step, apple-on-the-tail, pending-turn-straight-back, queued-turn-straight-back-from-the-pending-turn, ...), several-violations-are-listed-in-order and reversed-pending-turn-and-reversed-queue-are-both-listed.

Watch out: snake-no-overlap and snake-connected are different. A snake with the same cell twice in a row (doubled-cell-counts-as-overlap-and-as-disconnected) breaks both: the cells overlap, and they are zero steps apart, not one. Reuse inBounds from Module 3 and contains from Module 1. queued-not-reversed compares with nextDir, not with dir: in a-queued-turn-is-fine the snake moves Right, Up is pending and Left is queued, which is fine.

Exercise 12.5 — moveGaps

JavaScript

export const moveGaps = (states) => ...       // number[]

Scala

def moveGaps(states: List[GameState]): List[Int]

F#

let moveGaps (states: GameState list) : int list

Tests: moveGaps measures the distance between consecutive moves of the head, moveGaps of fewer than two moves is empty.

Exercise 12.6 — genSnake

JavaScript

export const genSnake = (width, height, maxLen) => ...   // Random<Point[]>, head first; maxLen >= 1

Scala

def genSnake(width: Int, height: Int, maxLen: Int): Random[List[Point]]

F#

let genSnake (width: int) (height: int) (maxLen: int) : Random<Point list>

Draw exactly as section 7 and the stub's doc comment say: the head's x, then its y, then one elementOf per further cell among the free in-bounds neighbours of the last cell, in the order Up, Down, Left, Right; stop at maxLen cells or when there is no candidate.

Tests: genSnake draws the head first, then walks from the tail (seed 0, 5x5, at most 6 cells), genSnake is pinned for a few more seeds, genSnake with maxLen 1 is just the head, drawn with two draws, genSnake stops early when the walk is stuck: a 1x1 board holds one cell, genSnake always gives a snake on the board, connected, without overlap, at most maxLen long, and, through the given genState, every generated state is sane: 500 states of a 5x5 board have no violations and generated states are Playing, have nothing queued, and vary in length and apple.

Watch out: the walk extends the snake at its tail (the last cell), and the snake is head first, so new cells go at the end of the list. Stopping early must not use up a draw: when there are no candidates, return the snake with pure. And do not draw the head as one random cell from a list of all cells: that is a different draw, and the pinned tests will tell you so.

Exercise 12.7 — advanceSpec

JavaScript

export const advanceSpec = (state) => ...      // GameState; must equal advance(state) on every sane state

Scala

def advanceSpec(state: GameState): GameState

F#

let advanceSpec (state: GameState) : GameState

Write it as section 8 describes, without calling advance: build the snake the step would produce, then let violations decide whether it contains snake-in-bounds or snake-no-overlap.

Tests: advanceSpec agrees with Module 3's advance fixture: … (one test per case of fixtures/m03-advance.json), advance and advanceSpec agree on 500 generated states of a 5x5 board, no invariant sees the wrong collision check of Puzzle 1: every state it produces is sane, comparing with advanceSpec catches the wrong collision check: the head was moving onto the tail.

Watch out: ask violations about the state with the new snake, and look only at the two snake invariants. When the step eats, the new head is on the apple, so apple-not-on-snake is in the list too, and that does not make the step deadly. Game over keeps the old snake and records dir = nextDir, exactly as in Module 3.

The payoff

When 12.1–12.5 are green, the remaining tests of the module run your library against the game. They need no code from you; read them in the test file, because they show how the pieces are used together:

• the real game keeps every invariant on 300 random games of 40 actions;
• the quick double turn bug is found and shrunk to its two key presses;
• a game without walls is found and shrunk to the shortest way off the board: ten ticks;
• a Tick that forgets the queued turn is caught by queued-not-reversed and shrunk to four actions;
• a queue that accepts a reversal is found and shrunk to its two key presses;
• the real game moves exactly every movesEvery(score) frames, also across a speed-up;
• counting frames from the start of the game makes some steps too short, and the property finds one.

If the first of these fails, do not assume that your library is wrong. It may have found a real bug in your rules that the fixtures missed. Shrink the counterexample and look at it.

Run

• JS: cd js && node --test "test/m12-*.test.js"
• Scala: cd scala && ./test.sh M12
• F#: cd fsharp && ./test.sh M12

Hints

Exercise 12.1 (elementOf, listOf) — nudge

elementOf is "a random index, transformed into the element at that index". listOf is recursion on n: what is a list of zero draws, and how do you get a list of n draws from one draw and a list of n - 1 draws?

Exercise 12.1 (elementOf, listOf) — stronger hint

elementOf(xs): map over intBelow(length of xs). listOf(gen, n): if n is 0 (or less), pure of the empty list. Otherwise flatMap over gen; inside, you have the first value a and need a Random of the whole list: map over listOf(gen, n - 1) and put a in front. In F# remember that the function is bind and that the data comes last.

Exercise 12.1 (elementOf, listOf) — near-solution (try the others first)

export const elementOf = (xs) => map(intBelow(___), (i) => ___)
export const listOf = (gen, n) =>
  n <= 0 ? pure(___) : flatMap(gen, (a) => map(listOf(gen, ___), (rest) => [___, ...___]))

def elementOf[A](xs: List[A]): Random[A] = Random.intBelow(___).map(i => ___)
def listOf[A](gen: Random[A], n: Int): Random[List[A]] =
  if n <= 0 then Random.pure(___)
  else gen.flatMap(a => listOf(gen, ___).map(rest => ___ :: ___))

let elementOf (xs: 'a list) : Random<'a> = Random.intBelow ___ |> Random.map (fun i -> List.item i xs)
let rec listOf (n: int) (gen: Random<'a>) : Random<'a list> =
    if n <= 0 then Random.pure ___
    else gen |> Random.bind (fun a -> listOf ___ gen |> Random.map (fun rest -> ___ :: ___))

Exercise 12.2 (forAll) — nudge

Write a helper that takes the number of the current run and the current seed. It has three outcomes: all runs are done; this value passes, so go on with the next run and the leftover seed; this value fails, so report.

Exercise 12.2 (forAll) — stronger hint

go(i, s): if i has reached runs, the result is the success report. Otherwise run gen with s to get the value and the next seed. If prop(value) holds, the result is go(i + 1, nextSeed). If not, the result is the failure report with i, s (not nextSeed) and the value. forAll is go(0, seed). In Scala, mark the helper @annotation.tailrec; in F#, let rec with the recursive call in tail position.

Exercise 12.2 (forAll) — near-solution (try the others first)

export const forAll = (gen, prop, runs, seed) => {
  const go = (i, s) => {
    if (i >= runs) return { ok: true, runs }
    const [value, next] = run(gen, s)
    return prop(value) ? go(___, ___) : { ok: false, run: ___, seed: ___, value }
  }
  return go(0, seed)
}

def forAll[A](gen: Random[A], runs: Int, seed: Long)(prop: A => Boolean): CheckResult[A] =
  @annotation.tailrec
  def go(i: Int, s: Long): CheckResult[A] =
    if i >= runs then CheckResult.Passed(runs)
    else
      val (value, next) = gen.run(s)
      if prop(value) then go(___, ___) else CheckResult.Failed(___, ___, value)
  go(0, seed)

let forAll (runs: int) (seed: uint32) (prop: 'a -> bool) (gen: Random<'a>) : CheckResult<'a> =
    let rec go i s =
        if i >= runs then Passed runs
        else
            let (value, next) = Random.run s gen
            if prop value then go ___ ___ else Failed(___, ___, value)
    go 0 seed

Exercise 12.3 (removals, minimize) — nudge

removals: for each index, the list without the element at that index. minimize: find the first removal that still fails; what do you do with it, and what do you do when there is none?

Exercise 12.3 (removals, minimize) — stronger hint

removals in JS: map with the index, and build each list from two slices. In Scala, xs.indices.toList.map(i => xs.patch(i, Nil, 1)); in F#, List.mapi with List.removeAt (or recursion on the list: removing from x :: rest is either rest, or x in front of each removal of rest). minimize: find (List.tryFind) the first failing removal. If there is one, the answer is minimize of it. If not, the answer is xs.

Exercise 12.3 (removals, minimize) — near-solution (try the others first)

export const removals = (xs) => xs.map((_, i) => [...xs.slice(0, ___), ...xs.slice(___)])
export const minimize = (xs, fails) => {
  const smaller = removals(xs).find(___)
  return smaller === undefined ? ___ : minimize(___, fails)
}

def removals[A](xs: List[A]): List[List[A]] = xs.indices.toList.map(i => xs.patch(i, Nil, ___))
def minimize[A](xs: List[A])(fails: List[A] => Boolean): List[A] =
  removals(xs).find(___) match
    case Some(smaller) => minimize(___)(fails)
    case None          => ___

let removals (xs: 'a list) : 'a list list = xs |> List.mapi (fun i _ -> List.removeAt ___ xs)
let rec minimize (fails: 'a list -> bool) (xs: 'a list) : 'a list =
    match removals xs |> List.tryFind ___ with
    | Some smaller -> minimize fails ___
    | None -> ___

Exercise 12.4 (violations) — nudge

Do not write eight ifs that push onto a list. Write a table: a list of pairs (name, a function that says whether the state is fine). Then the result is "the names of the pairs whose function says no".

Exercise 12.4 (violations) — stronger hint

The predicates, on a state s: the snake's length is above 0; every snake cell satisfies inBounds; for every cell, the cells after it do not contain it; every cell from the second on is a neighbour of the cell before it (the sum of the absolute differences of x and y is exactly 1); the apple is absent or in bounds; the apple is absent or not contained in the snake; nextDir differs from opposite(dir); queued is absent or differs from opposite(nextDir). For "each cell and the one before it", pair the snake with itself shifted by one: in JS use the index argument of every, in Scala snake.zip(snake.drop(1)), in F# List.pairwise.

Exercise 12.4 (violations) — near-solution (try the others first)

const neighbours = (a, b) => Math.abs(a.x - b.x) + Math.abs(a.y - b.y) === 1
const invariants = [
  ['snake-not-empty', (s) => s.snake.length > 0],
  ['snake-in-bounds', (s) => s.snake.every((p) => ___)],
  ['snake-no-overlap', (s) => s.snake.every((p, i) => !contains(s.snake.slice(___), p, pointEquals))],
  ['snake-connected', (s) => s.snake.slice(1).every((p, i) => neighbours(s.snake[___], p))],
  ['apple-in-bounds', (s) => s.apple === null || ___],
  ['apple-not-on-snake', (s) => s.apple === null || ___],
  ['turn-not-reversed', (s) => ___],
  ['queued-not-reversed', (s) => s.queued === null || ___],
]
export const violations = (state) => invariants.filter(([, holds]) => ___).map(([name]) => name)

The Scala and F# versions have the same shape: a List of (String, GameState => Boolean) pairs, then filterNot/List.filter and map. With snake.zip(snake.drop(1)).forall { case (a, b) => ... } or List.pairwise snake |> List.forall (fun (a, b) -> ...) for the connected check, and apple.forall(p => ...) / Option.forall (fun p -> ...) apple for "absent or fine".

Exercise 12.5 (moveGaps) — nudge

Two steps. First the list of indices at which the head moved. Then the differences between neighbours in that list.

Exercise 12.5 (moveGaps) — stronger hint

Step 1: pair each state with the one before it (JS: map with the index, look at states[i - 1]; Scala: states.zip(states.drop(1)).zipWithIndex; F#: List.pairwise and List.indexed), keep the indices where the two heads differ. Mind the off-by-one: the pair of states 0 and 1 is a move at index 1. Step 2: pair the list of indices with itself shifted by one and subtract.

Exercise 12.5 (moveGaps) — near-solution (try the others first)

export const moveGaps = (states) => {
  const moved = states
    .map((s, i) => (i > 0 && !pointEquals(s.snake[0], states[___].snake[0]) ? i : -1))
    .filter((i) => i >= 0)
  return moved.slice(1).map((i, k) => i - moved[___])
}

def moveGaps(states: List[GameState]): List[Int] =
  val moved = states.zip(states.drop(1)).zipWithIndex.collect {
    case ((before, after), i) if before.snake.headOption != after.snake.headOption => ___
  }
  moved.zip(moved.drop(1)).map((a, b) => ___)

let moveGaps (states: GameState list) : int list =
    states
    |> List.pairwise
    |> List.indexed
    |> List.filter (fun (_, (before, after)) -> List.tryHead before.Snake <> List.tryHead after.Snake)
    |> List.map (fun (i, _) -> ___)
    |> List.pairwise
    |> List.map (fun (a, b) -> ___)

Exercise 12.6 (genSnake) — nudge

Write a helper that takes the snake built so far and the number of cells still allowed, and returns a Random of the finished snake. It has three outcomes: no cells left to add; no candidate cell; or pick a candidate and continue. genSnake draws the head and then calls the helper.

Exercise 12.6 (genSnake) — stronger hint

grow(snake, left): if left is 0 (or less), pure(snake). Otherwise take the last cell, move it in each of Up, Down, Left, Right (in that order), and keep the cells for which inBounds holds (it only reads width and height, so a small record with those two fields will do) and which the snake does not contain. No candidates: pure(snake). Otherwise flatMap over elementOf(candidates) and continue with the snake plus that cell and left - 1. genSnake is flatMap over intBelow(width), inside it flatMap over intBelow(height), and inside that grow([head], maxLen - 1).

Exercise 12.6 (genSnake) — near-solution (try the others first)

const directions = ['Up', 'Down', 'Left', 'Right']
const grow = (width, height, snake, left) => {
  if (left <= 0) return ___
  const last = snake[snake.length - 1]
  const options = directions
    .map((d) => move(last, d))
    .filter((p) => inBounds({ width, height }, p) && !___)
  return options.length === 0 ? ___ : flatMap(elementOf(options), (p) => grow(width, height, [___, p], ___))
}
export const genSnake = (width, height, maxLen) =>
  flatMap(intBelow(width), (x) => flatMap(intBelow(___), (y) => grow(width, height, [point(x, y)], ___)))

def genSnake(width: Int, height: Int, maxLen: Int): Random[List[Point]] =
  def grow(snake: List[Point], left: Int): Random[List[Point]] =
    val options = List(Direction.Up, Direction.Down, Direction.Left, Direction.Right)
      .map(d => Rules.move(snake.last, d))
      .filter(p => p.x >= 0 && p.x < width && p.y >= 0 && p.y < height && ___)
    if left <= 0 || options.isEmpty then Random.pure(___)
    else elementOf(options).flatMap(p => grow(snake :+ ___, ___))
  Random.intBelow(width).flatMap(x => Random.intBelow(___).flatMap(y => grow(List(Point(x, y)), ___)))

let genSnake (width: int) (height: int) (maxLen: int) : Random<Point list> =
    let rec grow (snake: Point list) (left: int) : Random<Point list> =
        let options =
            [ Up; Down; Left; Right ]
            |> List.map (fun d -> Rules.move (List.last snake) d)
            |> List.filter (fun p -> p.X >= 0 && p.X < width && p.Y >= 0 && p.Y < height && ___)
        if left <= 0 || List.isEmpty options then Random.pure ___
        else elementOf options |> Random.bind (fun p -> grow (snake @ [ ___ ]) ___)
    Random.intBelow width |> Random.bind (fun x -> Random.intBelow ___ |> Random.bind (fun y -> grow [ { X = x; Y = y } ] ___))

Exercise 12.7 (advanceSpec) — nudge

Follow the Module 3 shape of compute, decide, build. Compute the new head, whether it eats, and the whole new snake. Decide by asking violations about the state with that snake. Build one of the two results.

Exercise 12.7 (advanceSpec) — stronger hint

Not Playing: return the state. head = move(snake[0], nextDir); eating = the apple is there and equals head; snake' = [head, ...(eating ? snake : dropLast(snake))]. broken = violations of the state with snake' contains 'snake-in-bounds' or 'snake-no-overlap'. If broken: the state with dir: nextDir and status: 'GameOver'. Otherwise: the state with snake', dir: nextDir, the apple gone if eating, and the score plus one if eating.

Exercise 12.7 (advanceSpec) — near-solution (try the others first)

export const advanceSpec = (state) => {
  if (state.status !== 'Playing') return state
  const head = move(state.snake[0], state.nextDir)
  const eating = state.apple !== null && pointEquals(head, state.apple)
  const snake = [head, ...(eating ? ___ : ___)]
  const broken = violations({ ...state, snake }).some((v) => v === ___ || v === ___)
  return broken
    ? { ...state, dir: state.nextDir, status: ___ }
    : { ...state, snake, dir: state.nextDir, apple: ___, score: ___ }
}

def advanceSpec(state: GameState): GameState =
  if state.status != Status.Playing then state
  else
    val head = Rules.move(state.snake.head, state.nextDir)
    val eating = state.apple.contains(head)
    val snake = head :: (if eating then ___ else ___)
    val broken = violations(state.copy(snake = snake)).exists(v => v == ___ || v == ___)
    if broken then state.copy(dir = state.nextDir, status = ___)
    else state.copy(snake = snake, dir = state.nextDir, apple = ___, score = ___)

let advanceSpec (state: GameState) : GameState =
    if state.Status <> Playing then state
    else
        let head = Rules.move (List.head state.Snake) state.NextDir
        let eating = state.Apple = Some head
        let snake = head :: (if eating then ___ else ___)
        let broken = violations { state with Snake = snake } |> List.exists (fun v -> v = ___ || v = ___)
        if broken then { state with Dir = state.NextDir; Status = ___ }
        else { state with Snake = snake; Dir = state.NextDir; Apple = ___; Score = ___ }

Check your understanding

1. forAll returns a report instead of throwing an exception. Name two things you can do with a report that you could not do if the test runner printed "FAILED" and exited.
2. A colleague's random test fails once a week on the build server and never on their laptop. Which hidden inputs would you look for? Why can that not happen to forAll(genActions(40), prop, 300, 2024)?
3. Write listOf for IO instead of Random (on paper): replicate(io, n) : IO<A[]>. Which lines change? What does that tell you about flatMap and pure?
4. Predict, without running anything: minimize([1, 2, 3, 4], xs => xs.length >= 2) and minimize([1, 2, 3], xs => xs.length === 1 || xs.length === 3). Which of the two results is the smallest failing list that exists?
5. The replay law replay(s, a ++ b) == replay(replay(s, a), b) holds for every update function. Explain why, and then decide for each of these whether a broken game could fail it: (a) history(s, as) ends with replay(s, as); (b) update(s, Tick) never changes width or height; (c) the score never goes down; (d) update(update(s, TogglePause), TogglePause) == s for every state s. Is (d) even true?
6. The wrong collision check of Puzzle 1 (Module 3), "the new head must not be on the old snake", keeps every invariant of this module, and Exercise 12.7 catches it by comparison with advanceSpec. Explain why no invariant of a single state can catch it. Then design the other kind of property the original version of this question suggested: a sequence of actions from a hand-built start state on a small board that must be survivable. Which of the two would still find the bug if advanceSpec had been written with the same mistake?
7. Random play from newGame almost never reaches score 3. Describe two different ways to get test games that do: one that changes the generator, one that changes the start state. Which did the tests of this module choose, and why?
8. violations checks eight invariants at run time. Pick one of them and sketch a data model in which a state that breaks it cannot be built at all. What does your model cost in the rest of the code? (Example to start from: a snake stored as a head plus a list of directions cannot be disconnected.)
9. In the test the quick double turn bug is found and shrunk to its two key presses, the first key is Up or Down and the second is Left. Why can the shrunk list not contain a Tick? And why is the second key never Right?
10. Trace the counterexample of a Tick that forgets the queued turn is caught by queued-not-reversed and shrunk to four actions (Turn Up, Turn Right, Tick, Turn Left) state by state: dir, nextDir, queued after each action. Which invariant breaks, and after which action? What would the snake have done on the next step?
11. genState never produces a state with something queued. Extend it on paper so that it also produces states with a queued turn that the real game could reach. Which constraint must the queued direction satisfy, and which further constraint links it to dir?
12. With maxLen = 25 on a 5 x 5 board, is the snake from genSnake always 25 cells long? Why not? Does the answer matter for the comparison test of Exercise 12.7?
13. Why does the comparison test run on generated states rather than on the states of random games from newGame? Estimate roughly how often a random game of 40 actions brings the head next to its own tail with nextDir pointing at it.

In production

• QuickCheck (Haskell, 1999) is where this style of testing comes from; its generators are a monad over a splittable random seed, as ours are over a seed. Every mainstream language now has a descendant: fast-check for JavaScript and TypeScript, ScalaCheck for Scala, FsCheck for F# and C#, Hypothesis for Python.
• Shrinking in those libraries is more refined than minimize: they also make numbers smaller and strings shorter, and newer designs such as Hedgehog and Hypothesis shrink the random choices instead of the generated value, so that a shrunk value is always one the generator could have produced.
• Mutation testing tools such as Stryker (JavaScript, C#, Scala) change your code automatically, one operator at a time, and report the changes that no test notices. (This course's own test suite was checked that way; the surviving mutants became new fixture cases, for example the Pong cases ball-in-column-zero-is-still-in-play and player-paddle-catches-the-ball-at-its-first-row.)
• Deterministic simulation testing takes "same seed, same run" to the scale of a distributed database: the whole cluster, with its network and disks, runs inside one deterministic simulation driven by a seed, so that a failure found after millions of simulated hours can be replayed exactly. FoundationDB was built this way (Simulation and Testing). It is the idea of Module 5, applied to a data centre.
• Model checkers explore every reachable state of a model instead of a random sample, and are the next step when "300 random games passed" is not enough (TLA+).

Further reading

• Koen Claessen and John Hughes, "QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs" — the original paper (ICFP 2000); sections 1–3 are readable with this course behind you, and its Gen is your Random.
• Scott Wlaschin, "Choosing properties for property-based testing" — a catalogue of property shapes ("there and back again", "some things never change", "the test oracle") with pictures.
• Andreas Zeller, "Reducing Failure-Inducing Inputs" (The Debugging Book) — delta debugging, the general form of minimize, by its inventor.
• fast-check documentation — what a production library adds: many generators, integrated shrinking, replay of a failure from its seed.
• Mutation testing (Wikipedia) and Metamorphic testing (Wikipedia) — testing the tests, and testing relations between runs when no expected output is known.
• Philip Wadler, "Theorems for free!" — why some properties (like the replay law) hold for every function of a given type, and so cannot fail.
• Hillel Wayne, "Learn TLA+" — an introduction to checking all states of a design instead of sampling them.