Write you some QuickCheck - Properties

This post is part of a series of posts on implementing a minimal version of QuickCheck from scratch. The source code is available on GitHub.

Prelude

In QuickCheck the programmer writes assertions about logical properties that a function should fulfill.

Take List.rev as an example, which is a function that returns a new list with the elements in reverse order:

List.rev [1; 2; 3];;

val it : int list = [3; 2; 1]

One logical property of List.rev is:

Calling List.rev twice must return the elements in the original order.

Here’s an example assertion:

List.rev (List.rev [1; 2; 3]) = [1; 2; 3];;

val it : bool = true

A generic assertion

In the previous example List.rev was tested against an example value [1; 2; 3]. To make the assertion generic, the example value can be parameterized as any list:

fun xs -> List.rev (List.rev xs) = xs;;

val it : xs:'a list -> bool when 'a : equality = <fun:clo@33>

QuickCheck will then attempt to generate a test case that falsifies the assertion. In order to do that, it needs to know which generator to use, to feed xs with random values.

A generator for lists of integers

Values for xs need to be generated by a generator. The following one is for lists of type integer:

let g = Gen.list Gen.int;;

val g : Gen<int list>

QuickCheck Properties

Every possible value generated by the g generator must now be supplied to the assertion, as shown below:

fun xs -> List.rev (List.rev xs) = xs
|> Property.forAll g;;

val it : Property

But what is forAll? This comes from predicate logic and essentially means that the assertion holds for all possible values generated by g:

let forAll (g : Gen<'a>) (f : ('a -> 'b)) : Property =
    Prop(gen {
             let!      x = g           (* Get 'a from the Gen<'a>. *)
             let! actual = f x         (* Apply the value 'a to f. *)
                           |> convert  (* Turn it into a Property. *)
                           |> evaluate (* Get the results from it. *)
             return { actual with Arguments = x.ToString() :: result.Arguments }
         })

In its simplest form, Property is a generator of Result, (Gen<Result>)¹, which means we can easily try out a Property just as we would do with a generator.

type Property =
    private
    | Prop of Gen<Result>

and Result =
    { Ok : option<bool>
      Arguments : list<string> }

Try out (see it pass)

Using only the Gen and Property modules, the assertion can be turned into a property and sampled:

fun xs -> xs |> List.rev |> List.rev = xs
|> Property.forAll g (* For each value generated by g, the property must hold. *)
|> Property.evaluate
|> Gen.sample;;

val it : Result list =
  [ { Status = Some true
      Args   = ["[]"] }

    { Status = Some true
      Args   = ["[0]"] }

    { Status = Some true
      Args = ["[-4; 2]"] }

    { Status = Some true
      Args   = ["[-5; -2; -5; ... ]"] }

    { Status = Some true
      Args   = ["[3]"] }

    { Status = Some true
      Args   = ["[4; 9; -5; ... ]"] }

    { Status = Some true
      Args   = ["[-1; 8; 9; ... ]"] }

    { Status = Some true
      Args   = ["[9; 0; -15; ... ]"] }

    { Status = Some true
      Args   = ["[-11; 18; -9; ... ]"] }
  ]
>

The assertion holds for all cases, which means the ‘test’ passes.

Try out (see it fail)

To see the ‘test’ fail, the assertion can be changed from

fun xs -> xs |> List.rev |> List.rev = xs

fun xs -> xs |> List.rev = xs

and run again:

fun xs -> xs |> List.rev = xs
|> Property.forAll g
|> Property.evaluate
|> Gen.sample;;

val it : Result list =
  [ { Status = Some true
      Args   = ["[]"] }

    { Status = Some false
      Args   = ["[1; -1]"] }

    { Status = Some false
      Args   = ["[-2; 2]"] }

    { Status = Some false
      Args   = ["[3; 3; -3; ... ]"] }

    { Status = Some false
      Args   = ["[-8; 9]"] }

    { Status = Some false
      Args   = ["[1; -6; 11; ... ]"] }

    { Status = Some false
      Args   = ["[-6; 16; -5; ... ]"] }

    { Status = Some false
      Args   = ["[-1; 8; 6; ... ]"] }

    { Status = Some false
      Args   = ["[4; 8; -8; ... ]"] }
  ]
>

The test now fails. — But, there’s some noise in the results; the counter-example isn’t obvious.

It’d be wise if we can clean the noise by trying to report back the minimal counter-example. This process is called shrinking and will be shown over the next post(s).

To support shrinking, a Property needs to hold more information. As an example, see the Property in QuickCheck 2. ↩