moodmosaic (@nikosbaxevanis)
Blog About Projects Bookmarks Tags

# 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>`)1, 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   = [""] }

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

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

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

{ 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
``````

to

``````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).

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

━━━

This post has been filed under f# quickcheck

© 2016-05-27 Nikos Baxevanis <nikos.baxevanis@gmail.com>