Lecture 10 — Property-based testing

Introduction

Designing, implementing and reasoning about large systems requires abstraction.

We treat a component as a black box (hiding the implementation) and are only interested in its behaviour (external interface): what does it require, what does it guarantee.

Assumption: components adhere to their specification.

Property-based testing: we specify (propose, hypothesise) a property of a component, and the tool tries to falsify it (using randomness).

A "side effect" of testing in this style is that the specification of a component is made explicit (a set of properties).

1 · Properties

What is a property?

In property-based testing, a property is a falsifiable statement about the behaviour of a component. We express this statement in the host language (via an embedded domain-specific language).

Two non-examples:

• Every accepted job eventually completes. No finite test can falsify it.
• The system is reliable when operated correctly. What counts as a failure is not defined.

Say that we are testing a sorting function. How can we conclude that it is implemented incorrectly? What observation would falsify the claim that it is implemented correctly?

• Property: for all xs : 'a list, List.sort xs is a permutation of xs. Falsification: a list ys (a counterexample) such that List.sort ys is not a permutation of ys.
• Property: for all xs : 'a list, List.sort xs is non-decreasing. Falsification: a list ys such that List.sort ys is not non-decreasing.

Simple properties

Given a function f : 'a -> 'b, a simple property about f is a predicate on 'a (a function of type 'a -> bool).

For example, with List.rev : 'a list -> 'a list as f, what property does this predicate of type 'a list -> bool express?

let p1 xs = List.length (List.rev xs) = List.length xs

let p1Example = p1 [1; 2; 3]

true

The body checks that the length of the reversal of xs is the length of xs: reversing a list preserves the length.

Concrete example

List.rev is its own inverse. FsCheck is a NuGet package; a script gets it with one directive (the first run needs the network, later runs use the package cache):

#r "nuget: FsCheck, 3.6.0"
open FsCheck
open FsCheck.FSharp

let revRevIsId (xs: int list) = List.rev (List.rev xs) = xs

FsCheck tries to falsify this property (find a counterexample). It generates a list ys : int list. If revRevIsId ys = false, it has found a counterexample and stops; otherwise it continues, by default for up to 100 tests.

In F# Interactive, Check.Quick revRevIsId runs the check. Every run of Check.Quick uses a fresh random seed. These notes fix the seed, so that the page shows the same run every time; Check.One (seeded, p) is Check.Quick p with a fixed seed, and your own runs will differ:

let seeded = Config.Quick.WithReplay (Some { Rnd = Rnd (2026UL, 11UL); Size = None })

Check.One (seeded, revRevIsId)

Ok, passed 100 tests.

What inputs are generated?

Check.Verbose also prints every generated input. The first five tests:

let seededVerbose =
  Config.Verbose
    .WithReplay(Some { Rnd = Rnd (2026UL, 11UL); Size = None })
    .WithMaxTest(5)
    .WithEndSize 8

Check.One (seededVerbose, revRevIsId)

0:
[]
1:
[]
2:
[-4; 0; 0; 0; 0]
3:
[]
4:
[0; -2; 0; -1]
Ok, passed 5 tests.

Failing property

Is the reversal of xs @ ys related to the reversal of xs and ys?

let revAppendWrong (xs: int list) (ys: int list) =
  List.rev (xs @ ys) = List.rev xs @ List.rev ys

Check.One (seeded, revAppendWrong)

Falsifiable, after 2 tests (2 shrinks) (2026,11). 
Last step was invoked with size of 3 and seed of (6705859008916805902,1535923343514018517).
Replay directly at failing step with (6705859008916805902,1535923343514018517,3).
Original:
[-2; 0]
[-1]
Shrunk:
[0]
[1]
with exception:
System.Exception: Expected true, got false.

Falsified: [0] and [1] is a counterexample. The halves swap:

let revAppend (xs: int list) (ys: int list) =
  List.rev (xs @ ys) = List.rev ys @ List.rev xs

Check.One (seeded, revAppend)

Ok, passed 100 tests.

Broken implementation

NonNegativeInt is a single-constructor union provided by FsCheck: its values are the non-negative integers, so the type of the parameter keeps the input in range.

let rec fact n =
  match n with
  | 0 -> 1
  | 7 -> fact 6
  | n -> n * fact (n - 1)

let factStep (NonNegativeInt n) = fact (n + 1) = (n + 1) * fact n

Check.One (seeded, factStep)

Falsifiable, after 7 tests (0 shrinks) (2026,11). 
Last step was invoked with size of 8 and seed of (7552811758107635607,742021167357823125).
Replay directly at failing step with (7552811758107635607,742021167357823125,8).
Original:
NonNegativeInt 6
with exception:
System.Exception: Expected true, got false.

While fact n computes an incorrect result when n >= 7, factStep only fails on NonNegativeInt 6: for larger n, both sides are wrong by the same factor.

When are two lists equal?

revRevIsId passed 100 tests: FsCheck generated 100 values ys : int list, and for all of them List.rev (List.rev ys) = ys evaluated to true.

Lists are polymorphic in the type of their elements. Reversing a list of, say, strings should behave the same as reversing a list of integers. Can we conclude that List.rev (List.rev xs) = xs for all lists xs?

let revRevIsIdFloat (xs: float list) = List.rev (List.rev xs) = xs

Check.One (seeded, revRevIsIdFloat)

Falsifiable, after 16 tests (11 shrinks) (2026,11). 
Last step was invoked with size of 17 and seed of (8531533158813906174,8482786554965388143).
Replay directly at failing step with (8531533158813906174,8482786554965388143,17).
Original:
[-0.0; 0.0; 0.0; 0.0; -1.242624215; nan; -0.0; nan; 0.2610306871; 0.0;
 -4.97824528; -0.0]
Shrunk:
[nan]
with exception:
System.Exception: Expected true, got false.

No. The shrunk counterexample is [nan], and nan is not equal to itself:

let nanIsNan = nan = nan

false

2 · Shrinking and replay

Counterexamples

By default, Check.Quick starts from "small" inputs. If the generated input is not a counterexample, then the next input may be slightly "larger".

Since the search for counterexamples (test data generation) is not exhaustive, the first counterexample we find might not be the best explanation of the root cause.

Once FsCheck has found a counterexample, it tries to find a "smaller" counterexample by "shrinking" the current counterexample. A "smaller" counterexample hopefully is a better explanation.

Shrinking a value

To shrink a value x : 'a means to propose other candidate values of type 'a that we consider to be "smaller" than x. This mechanism is a function of type 'a -> 'a seq, the "shrinker".

If the first proposed value is also a counterexample, FsCheck recursively shrinks that. Otherwise it considers the next proposed value.

FsCheck's arbitrary for int carries its shrinker. What are some values "smaller" than 10 that we could try?

let intArb = ArbMap.arbitrary<int> ArbMap.defaults

let shrink10 = intArb.Shrinker 10 |> Seq.toList

[0; 5; 8; 9]

Suppose that 0 is not a counterexample but 5 is. Then FsCheck shrinks 5:

let shrink5 = intArb.Shrinker 5 |> Seq.toList

[0; 3; 4]

Shrinking a list

A list shrinks in two ways: shrink the data structure itself, or shrink the values in it.

let intListArb : Arbitrary<int list> = ArbMap.arbitrary ArbMap.defaults

let shrink321 = intListArb.Shrinker [3; 2; 1] |> Seq.toList

[[2; 1]; [3; 1]; [3; 2]; [0; 2; 1]; [2; 2; 1]; [3; 0; 1]; [3; 1; 1]; [3; 2; 0]]

The first three candidates are the original list with one element left out. The rest are lists that are otherwise exactly the same as the original except that one element has been replaced with a "smaller" element:

let shrink3 = intArb.Shrinker 3 |> Seq.toList
let shrink2 = intArb.Shrinker 2 |> Seq.toList

[0; 2]

[0; 1]

Shrinking example

WithEveryShrink directs FsCheck to print every successful shrinking step. Below, the printed lists are aligned, so that the gap in each line shows the element that step left out:

Check.One (seeded.WithEveryShrink (sprintf "%A\n"), revRevIsIdFloat)

[[0.0; 0.0; 0.0; -1.242624215; nan; -0.0; nan; 0.2610306871; 0.0; -4.97824528; -0.0]]
[[     0.0; 0.0; -1.242624215; nan; -0.0; nan; 0.2610306871; 0.0; -4.97824528; -0.0]]
[[          0.0; -1.242624215; nan; -0.0; nan; 0.2610306871; 0.0; -4.97824528; -0.0]]
[[               -1.242624215; nan; -0.0; nan; 0.2610306871; 0.0; -4.97824528; -0.0]]
[[                             nan; -0.0; nan; 0.2610306871; 0.0; -4.97824528; -0.0]]
[[                                  -0.0; nan; 0.2610306871; 0.0; -4.97824528; -0.0]]
[[                                        nan; 0.2610306871; 0.0; -4.97824528; -0.0]]
[[                                        nan;               0.0; -4.97824528; -0.0]]
[[                                        nan;                    -4.97824528; -0.0]]
[[                                        nan;                                 -0.0]]
[[                                        nan                                      ]]
Falsifiable, after 16 tests (11 shrinks) (2026,11). 
Last step was invoked with size of 17 and seed of (8531533158813906174,8482786554965388143).
Replay directly at failing step with (8531533158813906174,8482786554965388143,17).
Original:
[-0.0; 0.0; 0.0; 0.0; -1.242624215; nan; -0.0; nan; 0.2610306871; 0.0;
 -4.97824528; -0.0]
Shrunk:
[nan]
with exception:
System.Exception: Expected true, got false.

Each step leaves out one element and the property still fails, until only nan is left.

Remove from BST

From Lecture 6, the tree, its insert (here insertTree) and inOrder, and from Lecture 9 build:

type 'a BinTree = Empty
                | Node of 'a BinTree * 'a * 'a BinTree

let rec insertTree x t =
  match t with
  | Empty -> Node (Empty, x, Empty)
  | Node (l, y, r) ->
      match compare x y with
      | 0 -> t
      | c when c < 0 -> Node (insertTree x l, y, r)
      | _ -> Node (l, y, insertTree x r)

let rec inOrder t =
  match t with
  | Empty -> []
  | Node (l, x, r) ->
      inOrder l @ [x] @ inOrder r

let build xs = List.fold (fun acc x -> insertTree x acc) Empty xs

build xs is a search tree for any list xs. This remove contains a bug: at the value, it keeps only the left subtree.

let rec remove x t =
  match t with
  | Empty -> Empty
  | Node (l, y, r) ->
      if   x < y then Node (remove x l, y, r)
      elif x > y then Node (l, y, remove x r)
      else l

Removing x must keep every other value:

let removeKeepsOthers (x: int) (xs: int list) =
  let t = build xs
  inOrder (remove x t) = List.filter (fun y -> y <> x) (inOrder t)

Check.One (seeded, removeKeepsOthers)

Falsifiable, after 41 tests (13 shrinks) (2026,11). 
Last step was invoked with size of 42 and seed of (1349500317379569017,699349187029105039).
Replay directly at failing step with (1349500317379569017,699349187029105039,42).
Original:
1
[0; 0; -1; 1; 0; 1; 0; 29; 0]
Shrunk:
0
[0; 1]
with exception:
System.Exception: Expected true, got false.

A shrunk counterexample

The original list gives the tree on the left; the shrunk list [0; 1] gives the tree on the right.

Removing 0 from the shrunk tree also drops 1: the result is the left subtree, which is Empty. The shrunk counterexample directly points to the issue.

Reading a report

The report on revRevIsIdFloat again:

Check.One (seeded, revRevIsIdFloat)

Falsifiable, after 16 tests (11 shrinks) (2026,11). 
Last step was invoked with size of 17 and seed of (8531533158813906174,8482786554965388143).
Replay directly at failing step with (8531533158813906174,8482786554965388143,17).
Original:
[-0.0; 0.0; 0.0; 0.0; -1.242624215; nan; -0.0; nan; 0.2610306871; 0.0;
 -4.97824528; -0.0]
Shrunk:
[nan]
with exception:
System.Exception: Expected true, got false.

• Falsifiable, after 16 tests: the sixteenth input that was generated falsified the property; (2026,11) is the seed of the whole run.
• 11 shrinks: FsCheck found 11 smaller inputs, each still failing.
• Last step: the seed and size of the failing test.
• Replay directly: the seed and size that regenerate exactly that input.
• Original: the first input that failed, one line per parameter.
• Shrunk: the smallest failing input found.

Replay

The report printed the seed and size of the failing step. A configuration with that seed and size regenerates the same input:

let failingSeed = Rnd (8531533158813906174UL, 8482786554965388143UL)

let replayFailure =
  Config.Quick.WithReplay (Some { Rnd = failingSeed; Size = Some 17 })

Check.One (replayFailure, revRevIsIdFloat)

Falsifiable, after 1 test (11 shrinks) (8531533158813906174,8482786554965388143). 
Last step was invoked with size of 17 and seed of (8531533158813906174,8482786554965388143):
Original:
[-0.0; 0.0; 0.0; 0.0; -1.242624215; nan; -0.0; nan; 0.2610306871; 0.0;
 -4.97824528; -0.0]
Shrunk:
[nan]
with exception:
System.Exception: Expected true, got false.

We can reproduce the exact same search that found the counterexample.

3 · More on properties

Conditional properties

The properties so far are of the form \(\forall (x : X), P(x)\): we require every possible value \(x : X\) to have the property \(P\).

Sometimes we want to talk about a certain subset of the values \(x : X\). For example, we may want to say that those values \(x : X\) that satisfy the property \(P\) must satisfy the property \(Q\):

\(\forall (x : X), P(x) \implies Q(x)\)

For a particular x, with properties p and q, we could say if p x then q x else true. The FsCheck syntax for such properties is precondition ==> property.

Conditional properties (ctd.)

The following property should check that, for non-empty lists, the head element of the reversed list is the last element of the original list:

Check.One (seeded, fun (xs: int list) ->
  xs <> [] ==> (List.head (List.rev xs) = List.last xs))

Falsifiable, after 1 test (0 shrinks) (2026,11). 
Last step was invoked with size of 2 and seed of (9642087697066849451,7737682524261845263):
Original:
[]
with exception:
System.ArgumentException: The input list was empty. (Parameter 'list')

What went wrong? Arguments are evaluated before the function body. This applies to ==> as well, in particular also when xs = [].

Solution: wrap the property after ==> in lazy, so that it is evaluated only when its result is actually needed:

let headRevIsLast (xs: int list) =
  xs <> [] ==> lazy (List.head (List.rev xs) = List.last xs)

Check.One (seeded, headRevIsLast)

Ok, passed 100 tests.

headRevIsLast passes 100 tests. Note its type: int list -> Property, not int list -> bool.

How many tests were useful?

let palindrome xs = List.rev xs = xs

let headLastPalindrome (xs : int list) =
  (xs <> [] && palindrome xs) ==> lazy (List.head xs = List.last xs)

Check.One (seeded, headLastPalindrome)

Arguments exhausted after 9 tests.

FsCheck only managed to (non-trivially) test the property a few times.

A "trivial" test of p ==> q: if p is false, then the whole property is true no matter what q is. We care about the cases where q is tested.

FsCheck tried to test the property 100 times, but most of the generated lists were not palindromes and did not count. There is a limit on how many generated inputs can be rejected:

let maxRejected = Config.Quick.MaxRejected

1000

Ordered lists

let rec ordered (f : 'a -> 'a -> bool) (xs : 'a list) : bool =
  match xs with
  | [] | [ _ ]   -> true
  | x :: y :: xs -> f x y && ordered f (y :: xs)

let revFlipsOrder (xs : int list) =
  ordered (<=) xs ==> lazy (ordered (>=) (List.rev xs))

Check.One (seeded, revFlipsOrder)

Arguments exhausted after 25 tests.

Randomly generated lists are not likely to be ordered. Without a precondition, both of these pass:

let sortIsOrdered (xs : int list) = ordered (<=) (List.sort xs)

let revFlipsOrder2 (xs : int list) = ordered (>=) (List.rev (List.sort xs))

Check.One (seeded, sortIsOrdered)
Check.One (seeded, revFlipsOrder2)

Ok, passed 100 tests.
Ok, passed 100 tests.

Insert into ordered list

let rec insert ord x ys =
  match ys with
  | []      -> [ x ]
  | y :: ys -> if ord x y then x :: y :: ys else y :: insert ord x ys

let insertKeepsOrder (x: int) xs =
  ordered (<=) xs ==> lazy (ordered (<=) (insert (<=) x xs))

Check.One (seeded, insertKeepsOrder)

Arguments exhausted after 20 tests.

Prop.trivial marks the trivial tests, here the empty lists:

let insertTrivial (x: int) xs =
  ordered (<=) xs ==> lazy (ordered (<=) (insert (<=) x xs))
  |> Prop.trivial (List.length xs = 0)

Check.One (seeded, insertTrivial)

Arguments exhausted after 20 tests (20% trivial).

The percentage is out of the successful tests (the generated list xs was ordered, so the precondition was satisfied): in that share of them, xs was empty.

Classify generated data

Prop.classify counts the tests in a named class:

let insertClassify (x: int) xs =
  ordered (<=) xs ==> lazy (ordered (<=) (insert (<=) x xs))
  |> Prop.classify (ordered (<=) (x :: xs)) "at-head"
  |> Prop.classify (ordered (<=) (xs @ [ x ])) "at-last"

Check.One (seeded, insertClassify)

Arguments exhausted after 20 tests.
40% at-last.
40% at-head.
20% at-last, at-head.

A test can be in several classes. "at-head" counts the ordered lists where adding the generated element at the beginning gives an ordered list; "at-last" those where adding it at the end does.

Categorise generated data

Prop.collect counts the tests per value, here per length of xs:

let insertCollect (x: int) xs =
  ordered (<=) xs ==> lazy (ordered (<=) (insert (<=) x xs))
  |> Prop.collect (List.length xs)

Check.One (seeded, insertCollect)

Arguments exhausted after 20 tests.
60% 1.
20% 2.
20% 0.

Conjunctions, disjunctions, labels

We can form compound properties (conjunction p .&. q, disjunction p .|. q) and label the parts so that we know which of them failed:

let insertBothHeadTail (x: int) (xs : int list) =
  ordered (<=) xs ==>
  lazy ((Prop.label "head" <| ordered (<=) (x :: xs))
        .&.
        (Prop.label "tail" <| ordered (<=) (xs @ [x])))

Check.One (seeded, insertBothHeadTail)

Falsifiable, after 1 test (0 shrinks) (2026,11). 
Last step was invoked with size of 2 and seed of (9642087697066849451,7737682524261845263):
Label of failing property: tail
Original:
0
[1]
with exception:
System.Exception: Expected true, got false.

Expect an exception

Sometimes an exception is the expected result:

let expectDivideByZero x =
  Prop.throws<System.DivideByZeroException, _> (lazy (1 / (x - x)))

Check.One (seeded, expectDivideByZero)

Ok, passed 100 tests.

let expectDivideByZero' x =
  Prop.throws<System.DivideByZeroException, _> (lazy (1 / (x - 2)))

Check.One (seeded, expectDivideByZero')

Falsifiable, after 1 test (0 shrinks) (2026,11). 
Last step was invoked with size of 2 and seed of (9642087697066849451,7737682524261845263):
Original:
0
with exception:
System.Exception: Expected exception, none was thrown

4 · Generators

What are generators?

A generator of values of type X is a description of how to generate values of type X.

We can think of Gen<'a>, a generator of values of type 'a, as a function of type

int -> Randomness -> 'a

where the first argument bounds the size of the value to be generated and the second argument is a source of "randomness".

Why would we want to define our own generators and not use the default ones? Recall the properties about ordered lists. We can define a generator that is much more likely to generate an ordered list. This allows us to test such properties much more thoroughly.

FsCheck provides combinators for building complex generators from simpler ones.

Basic generators

Gen.constant ignores the size and randomness parameters and always generates the same value. As a function of type int -> Randomness -> 'a, think of it as fun s r -> 5.

let genFive : Gen<int> = Gen.constant 5

A key building block is Gen.choose : int * int -> Gen<int>. It ignores the size but uses randomness to pick a value from the given interval (with uniform distribution):

let smallPositive : Gen<int> = Gen.choose (1, 10)

Sample

As part of developing and testing a generator we often want to sample it to see what kind of data it generates. Gen.sample : int -> Gen<'a> -> 'a array takes the number of samples to produce and the generator to sample. These notes use Gen.sampleWithSeed (a seed, a size and the number of samples) to keep the page fixed:

let seed = Rnd (2026UL, 11UL)

let smallPositiveSample = Gen.sampleWithSeed seed 10 5 smallPositive

[|8; 3; 3; 10; 1|]

Gen.sample is not something to define a generator with; use it only to see what your generator would produce. Its result is not a generator, just an array. We build generators from other generators so that when the generator runs, the size and randomness arguments are propagated appropriately.

Gen.map

If we know how to generate values of type 'a and how to turn an 'a into a 'b, then we can generate values of type 'b: Gen.map : ('a -> 'b) -> Gen<'a> -> Gen<'b>.

let chooseFromList (xs: 'a list) : Gen<'a> =
  let idxGen = Gen.choose (0, List.length xs - 1)
  Gen.map (fun i -> List.item i xs) idxGen

Compare with Gen.elements : 'a seq -> Gen<'a>:

let fromListSample = Gen.sampleWithSeed seed 10 10 (chooseFromList [50 .. 100])
let elementsSample = Gen.sampleWithSeed seed 10 10 (Gen.elements [50 .. 100])

[|78; 53; 56; 67; 56; 79; 57; 76; 92; 67|]

[|78; 53; 56; 67; 56; 79; 57; 76; 92; 67|]

With the same seed, the two give the same sample.

Gen.bind

Gen.bind : ('a -> Gen<'b>) -> Gen<'a> -> Gen<'b> generates an 'a, then takes the generator of 'b-s for that particular 'a and generates a 'b. Which generator of 'b-s is used depends on the 'a that was generated (sequencing).

How do we generate a pair of integers where the first one is smaller than the second? Generate the first one, and then use a generator that can only generate larger numbers:

let larger i : Gen<int * int> =
  Gen.choose (i + 1, 100)
  |> Gen.map (fun j -> (i, j))

let ordPair : Gen<int * int> =
  Gen.choose (0, 99)
  |> Gen.bind larger

let ordPairSample = Gen.sampleWithSeed seed 10 5 ordPair

[|(67, 92); (12, 36); (60, 86); (84, 85); (3, 85)|]

Choosing a generator

Gen.oneof : Gen<'a> seq -> Gen<'a> first picks a generator, and that generator then generates the value. So Gen.oneof [ Gen.constant true; Gen.constant false ] is a Gen<bool> that, every time it needs to generate a value, first picks a generator.

Gen.frequency : (int * Gen<'a>) seq -> Gen<'a> controls the distribution: it picks a generator from a list of generators, weighting the probability of each by the given factor.

let boolGenOptimist = Gen.frequency [ (2, Gen.constant true); (1, Gen.constant false) ]

let optimistTrues =
  Gen.sampleWithSeed seed 10 100 boolGenOptimist |> Array.filter id |> Array.length

65

About two thirds of 100 samples are true.

Sized generators

Gen.sized : (int -> Gen<'a>) -> Gen<'a> takes a function that gives a generator for every possible size s : int. For example, natural numbers not larger than the given size:

let sizedNats s = Gen.choose (0, s)

We have a generator for every s : int. Gen.sized turns it into a generator of natural numbers that respects the size parameter:

let naturalGen = Gen.sized sizedNats

let naturalsAt10 = Gen.sampleWithSeed seed 10 10 naturalGen
let naturalsAt20 = Gen.sampleWithSeed seed 20 10 naturalGen
let naturalsAt100 = Gen.sampleWithSeed seed 100 10 naturalGen

[|4; 2; 8; 1; 4; 5; 8; 2; 7; 8|]

[|1; 0; 15; 5; 0; 11; 7; 14; 9; 20|]

[|94; 23; 16; 81; 89; 99; 77; 90; 59; 83|]

Arbitrary

An Arbitrary<'a> is the combination of a generator of 'a-s and a shrinker of 'a-s: Arb.fromGenShrink : Gen<'a> * ('a -> 'a seq) -> Arbitrary<'a>.

This is what FsCheck needs to try to falsify a property 'a -> bool: generate an arbitrary value of type 'a, and if it is a counterexample, try to shrink it. Custom generators should preferably also respect the size parameter.

• intArb of section 2 is FsCheck's arbitrary for int: intArb.Generator is a Gen<int>, and intArb.Shrinker an int -> int seq.
• Arb.fromGen makes a new arbitrary from a given generator, with an empty shrinker.
• Arb.fromGenShrink makes one from a given generator and shrinker.
• Arb.filter filters the generator and the shrinker.
• Arb.mapFilter maps and filters the generator, and filters the shrinker.

Quantified properties

Prop.forAll : Arbitrary<'a> -> ('a -> 'b) -> Property. Thus Prop.forAll arb p requires that every value a from arb satisfies the property p. By supplying a custom arbitrary we control the distribution of the test data:

let primeIsOdd =
  Prop.forAll (Arb.fromGen (chooseFromList [2; 3; 5; 7; 11; 13; 17; 19]))
              (fun p -> p % 2 = 1)

Check.One (seeded, primeIsOdd)

Falsifiable, after 4 tests (0 shrinks) (2026,11). 
Last step was invoked with size of 5 and seed of (12252048355222541855,11250175973109801033).
Replay directly at failing step with (12252048355222541855,11250175973109801033,5).
Original:
2
with exception:
System.Exception: Expected true, got false.

Arb.fromGen has an empty shrinker, so there were no shrinks.

Generating ordered lists

One way to generate ordered lists, without relying on filtering, starts from intListArb of section 2:

let orderedLists : Arbitrary<int list> = Arb.mapFilter List.sort (ordered (<=)) intListArb

Now we can say that for all x and for all ordered lists xs, insert x xs is an ordered list. We do not need a conditional property to exclude some of the generated data:

let insertKeepsOrder' x =
  Prop.forAll orderedLists (fun xs -> ordered (<=) (insert (<=) x xs))

Check.One (seeded, insertKeepsOrder')

Ok, passed 100 tests.

Generating recursive data

type Tree = Leaf of int
          | Branch of Tree * Tree

The FsCheck documentation provides a "naive" generator. It does not work:

let rec unsafeTree () =
  printfn "UNSAFE!"

  Gen.oneof
    [ Gen.map Leaf intArb.Generator
      Gen.map2
        (fun x y ->
          printfn "BRANCH"
          Branch(x, y))
        (unsafeTree ())
        (unsafeTree ()) ]

// unsafeTree () // Careful! Overflows the stack.

The call is commented out, so that the script runs to the end; remove the // to try it. Calling unsafeTree () evaluates the arguments of Gen.oneof first, including the two recursive calls unsafeTree (), before any tree is generated. Each of them does the same, so UNSAFE! is printed until the stack overflows, and BRANCH never is.

Tree generator that respects size

We define a function int -> Gen<Tree>, in other words a generator of trees for every s : int:

let rec treeWithSize (s: int) : Gen<Tree> =
  match s with
  | 0 -> Gen.map Leaf intArb.Generator
  | _ ->
      let subTreeGen = treeWithSize (s / 2)

      Gen.frequency
        [ (1, Gen.map Leaf intArb.Generator)
          (2, Gen.map2
                (fun left right -> Branch (left, right))
                subTreeGen
                subTreeGen) ]

let treeGen = Gen.sized treeWithSize

let treeSample = Gen.sampleWithSeed seed 10 1 treeGen

[|Branch
    (Leaf 5,
     Branch
       (Leaf 1, Branch (Branch (Leaf -1, Leaf 10), Branch (Leaf -1, Leaf 1))))|]

The values in the leaves come from intArb.Generator, in both places it is used; another generator there controls the values generated for the tree.

Computation expressions for generators

gen { ... } gives a more imperative notation for generators. let! x = g binds the value generated by g to x in the rest of the computation expression, and return v is a constant generator of v:

let ordPairGen =
  gen {
    let! j = Gen.choose (1, 100)
    let! i = Gen.choose (0, j - 1)
    return (i, j)
  }

let ordPairGenSample = Gen.sampleWithSeed seed 10 10 ordPairGen

[|(20, 68); (1, 13); (12, 61); (26, 85); (2, 4); (15, 33); (0, 33); (45, 50);
  (18, 20); (37, 58)|]

How this notation works: Lecture 11.

Patterns of properties

Where do properties come from? Some patterns recur. Each example below passes 100 tests unless it says otherwise.

There and back

Convert a value to some other value and then convert it back. Given f : S -> T and g : T -> S, is g (f s) = s? Is f (g t) = t? Serialisation, parsing and conversion are examples: different representations of the same thing.

let intRoundTrip (n: int) = int (string n) = n

Check.One (seeded, intRoundTrip)

Ok, passed 100 tests.

The other direction, string (int s) = s, does not hold. "007" is a number, but it does not come back as itself:

let back007 = string (int "007")

"7"

Maybe instead of equality we need to use some relation. For float, = is too strict because of nan, as in section 1. The method Equals treats nan as equal to itself:

let floatRoundTrip (x: float) = float (string x) = x
let floatRoundTripEquals (x: float) = (float (string x)).Equals x

Check.One (seeded, floatRoundTrip)
Check.One (seeded, floatRoundTripEquals)

Falsifiable, after 43 tests (0 shrinks) (2026,11). 
Last step was invoked with size of 44 and seed of (8536316237019846243,5574149147119119315).
Replay directly at failing step with (8536316237019846243,5574149147119119315,44).
Original:
nan
with exception:
System.Exception: Expected true, got false.
Ok, passed 100 tests.

Changing the order

Changing the order of some operations should not change the result: g (f x) = f (g x).

let left  (x, y) = (x + x, y)
let right (x, y) = (x, y * 2)

let leftRight (x: int, y: int) = left (right (x, y)) = right (left (x, y))

let mapRev (xs: int list) =
  List.rev (List.map ((+) 1) xs) = List.map ((+) 1) (List.rev xs)

Check.One (seeded, leftRight)
Check.One (seeded, mapRev)

Ok, passed 100 tests.
Ok, passed 100 tests.

Different ways of doing the same thing

Two different computations should give the same result:

let mapMap (xs: int list) =
  List.map ((+) 1) (List.map (( * ) 2) xs) = List.map ((+) 1 << ( * ) 2) xs

let sumOfLengths (xs: string list) =
  List.sum (List.map String.length xs) = String.length (String.concat "" xs)

Check.One (seeded, mapMap)
Check.One (seeded, sumOfLengths)

Ok, passed 100 tests.
Ok, passed 100 tests.

Some things stay the same

An "invariant" of a value does not change under the operation: invariant (f x) = invariant x. The length of a list is an invariant of List.map, and, as in section 1, of List.sort:

let mapKeepsLength (xs: int list) = List.length (List.map ((+) 1) xs) = List.length xs
let sortKeepsLength (xs: int list) = List.length (List.sort xs) = List.length xs

Check.One (seeded, mapKeepsLength)
Check.One (seeded, sortKeepsLength)

Ok, passed 100 tests.
Ok, passed 100 tests.

Twice is the same as once

Performing an operation twice is the same as performing it once ("idempotence"):

let distinctTwice (xs: int list) = List.distinct (List.distinct xs) = List.distinct xs
let sortTwice (xs: int list) = List.sort (List.sort xs) = List.sort xs

Check.One (seeded, distinctTwice)
Check.One (seeded, sortTwice)

Ok, passed 100 tests.
Ok, passed 100 tests.

Twice is the same as doing nothing

Performing an operation twice is the same as doing nothing ("involution"): revRevIsId of section 1. The identity function id satisfies the same property, but it is not List.rev:

let idIdIsId (xs: int list) = id (id xs) = xs

Check.One (seeded, idIdIsId)

Ok, passed 100 tests.

revAppend of section 1 tells them apart: id does not satisfy it.

let idAppend = id ([1] @ [2]) = id [2] @ id [1]

false

Look for a property that only the right function satisfies.

Compare with another implementation

The result should be the result of another implementation, for example a simpler or slower one ("test oracle"). Insertion sort, with insert of section 3, against List.sort:

let insertionSort xs = List.foldBack (insert (<=)) xs []

let sortsAgree (xs: int list) = insertionSort xs = List.sort xs

Check.One (seeded, sortsAgree)

Ok, passed 100 tests.

Summary

1. FsCheck tries to falsify a property.
2. A failing input is shrunk to a small counterexample.
3. Conditional properties (and filtering) require care. Measure.
4. Control test data distribution with custom generators.

Homework, reading and next week

Homework 6: defence this week.

Reading:

• the FsCheck documentation (we will assume that you are familiar with the API);
• Koen Claessen and John Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs (ICFP 2000);
• Scott Wlaschin's series The "Property Based Testing" series.