Write you some QuickCheck - Properties that hold under certain conditions

Jun 13, 2016

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.

In the previous post, we’ve seen how an assertion can be turned into a property and sampled, using only the Gen and Property modules:

fun x -> if x > 3 then true else false
|> Property.forAll g
|> Property.evaluate
|> Gen.sample;;

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

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

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

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

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

    { Status = Some false
      Args   = ["-5"] }

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

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

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

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

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

Notice that in this particular case, some tests passed:

val it : Result list =
  [ ...

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

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

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

    ...

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

while the rest of them failed:

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

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

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

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

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

    { Status = Some false
      Args   = ["-5"] }

    ...

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

    ...
  ]
>

In the assertion:

fun x -> if x > 3 then true else false

when we feed x with an integer that is lower then 3, the test fails.

In order to discard test cases where x is lower then 3, we use the ==> operator:

fun x -> x > 3 ==> if x > 3 then true else false

The ==> operator takes a predicate and a function, and returns a property that holds when the predicate returns true:

(* Returns a property that holds under certain conditions. Laws which are
   simple equations are conveniently represented by boolean functions but
   sometimes laws hold only under certain conditions. So this implication
   combinator represents such conditional laws. *)
let implies b x =
    if b then x |> convert
    else     () |> convert

let (==>) b x = implies b x

let private convert candidate =
    match box candidate with
    | :? Property   as p -> p
    | :? bool       as b -> boolProperty b
    | :? Lazy<bool> as b -> boolProperty b.Value
(* ... *) 
    | _                  -> unitProperty

Sample output

fun x -> x > 3 ==> if x > 3 then true else false
|> Property.forAll g
|> Property.evaluate
|> Gen.sample;;

val it : Property.Result list =
  [ { Status = null (* Discarded *)
      Args   = ["0"] }

    { Status = null (* Discarded *)
      Args   = ["2"] }

    { Status = null (* Discarded *)
      Args   = ["-3"] }

    { Status = null (* Discarded *)
      Args   = ["-4"] }

   { Status = null (* Discarded *)
     Args   = ["0"] }

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

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

   { Status = null (* Discarded *)
     Args   = ["1"] }

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

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

   { Status = null (* Discarded *)
     Args   = ["-2"] }
  ]
>

Tip: Using Lazy Computations

By default, F# expressions are evaluated exactly once when defined, however sometimes at most once semantics are needed, as shown below:

fun x -> x = x <> 0 ==> (1/x = 1/x)
|> Property.forAll g
|> Property.evaluate
|> Gen.sample

(* System.DivideByZeroException : Attempted to divide by zero. *)

In the above example, x can get the value 0, and although the test case is discared, the right part of the condition is eagerly evaluated. — In such cases, a lazy computation is required:

fun x -> x = x <> 0 ==> lazy (1/x = 1/x)
|> Property.forAll g
|> Property.evaluate
|> Gen.sample

(* Does not throw an exception. *)

val it : Property.Result list =
  [ { Status = null (* Discarded *)
      Args   = ["0"] }

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

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

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

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

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

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

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

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

   { Status = Some true
     Args   = ["-37"] }
  ]
>

Write you some QuickCheck - Properties

May 27, 2016

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   = ["[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

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.

Atom + Stack = no globally installed GHC/packages

May 19, 2016

When doing Haskell programming

Stack

The output should look like this:

$ stack setup
Downloaded lts-5.17 build plan.
Caching build plan
Fetching package index ...remote: Counting objects: 213332, done.
remote: Compressing objects: 100% (171913/171913), done.
Receiving objects: 100% (213332/213332), 49.84 MiB | 1.79 MiB/s, done.-reused 0

Resolving deltas: 100% (56842/56842), completed with 1 local objects.
From https://github.com/commercialhaskell/all-cabal-hashes
 * [new tag]         current-hackage -> current-hackage
Fetched package index.
Populated index cache.
Preparing to install GHC to an isolated location.
This will not interfere with any system-level installation.
ghc-7.10.3:   15.89 MiB / 128.40 MiB ( 12.37%) downloaded...

GHC installed to [..]\AppData\Local\Programs\stack\x86_64-windows\ghc-7.10.3\
stack will use a locally installed GHC
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
  • In the same directory as Stack.yaml execute stack build ghc-mod hlint stylish-haskell

atom-haskell

  • Install Atom
  • Install atom-haskell via apm: apm install language-haskell haskell-ghc-mod ide-haskell autocomplete-haskell ide-haskell-cabal
  • Start Atom via Stack from the command-line stack exec atom.cmd

That’s it – Happy Haskell programming!

Write you some QuickCheck - Shrinking lists

Apr 10, 2016

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.

In the previous post I’ve ported the function from QuickCheck that shrinks numbers. In this post I’ll be doing the same for lists.

Prelude

QuickCheck shrinks lists by dropping elements from them, given a shrinking function for individual elements.

shrinkList :: (a -> [a]) -> [a] -> [[a]]

-- (a -> [a]) the shrinker of type `a`.
--       [a]  the input to be shrinked.
--      [[a]] the output shrinked list.

Shrinking a list of integers

To shrink a list of integers, say [1,2,3] we need

  • a function that shrinks integers (shrinker)
  • a function that shrinks lists, applying for each element the shrinker

In Haskell QuickCheck 2.8.2, it looks like this:

-- A function that shrinks integers (the shrinker)
λ> :t shrinkIntegral
shrinkIntegral :: Integral a => a -> [a]

-- Examples
λ> shrinkIntegral 1
[0]

λ> shrinkIntegral 2
[0,1]

λ> shrinkIntegral 3
[0,2]

-- A function that shrinks lists (taking a shrinker and a list)
λ> :t shrinkList
shrinkList :: (a -> [a]) -> [a] -> [[a]]

-- Examples
λ> shrinkList shrinkIntegral [1]
[[],[0]]

λ> shrinkList shrinkIntegral [2]
[[],[0],[1]]

λ> shrinkList shrinkIntegral [3]
[[],[0],[2]]

λ> shrinkList shrinkIntegral [1,2]
[[],[2],[1],[0,2],[1,0],[1,1]]

λ> shrinkList shrinkIntegral [1,2,3]
[[],[2,3],[1,3],[1,2],[0,2,3],[1,0,3],[1,1,3],[1,2,0],[1,2,2]]

Doing similar in F#

A possible shrinking function for lists in F# can be based on the following Haskell code snippet, taken from QuickCheck 2.8.2:

shrinkOne []       = []
shrinkOne (x : xs) = [ x' : xs  |  x' <-       shr  x ]
                  ++ [ x  : xs' | xs' <- shrinkOne xs ]
module Shrink

(* A shrinker for values of type 'a. *)
type Shrink<'a> =
    | Shrink of ('a -> 'a seq)

(* Shrinks a sequence of elements of type 'a. First it yields an empty
   sequence, and then it iterates the input sequence, and shrinks each
   one of the items given the shrinker which is passed as a parameter. *)
let shrinkList xs (Shrink shr) =
    let rec shrinkImp xs =
        match xs with
        | []       -> Seq.empty
        | (h :: t) ->
            seq {
                yield []
                for h' in        shr h  -> h' :: t
                for t' in (shrinkImp t) -> h  :: t'
            }
    shrinkImp xs

I’m going to try this one with the same values as the ones used in Haskell:

(* A function that shrinks integers (the shrinker) *)
> let shrinker = Shrink shrinkNumber;;
val shrinker : Shrink<int> = Shrink <fun:shrinker@3>

(* A function that shrinks lists (taking a list and a shrinker) *)
val shrinkList : xs:'a list -> Shrink<'a> -> seq<'a list>

(* Examples *)
> shrinker |> shrinkList [1];;
val it : seq<int list> = seq [[]; [0]]

> shrinker |> shrinkList [2];;
val it : seq<int list> = seq [[]; [0]; [1]]

> shrinker |> shrinkList [3];;
val it : seq<int list> = seq [[]; [0]; [2]]

> shrinker |> shrinkList [1; 2];;
val it : seq<int list> = seq [[]; [0; 2]; [1]; [1; 0]; ...]

> shrinker |> shrinkList [1; 2; 3];;
val it : seq<int list> = seq [[]; [0; 2; 3]; [1]; [1; 0; 3]; ...]

Not exactly the same results as in Haskell, but similar. That’s because the shrinkList function in F# is based on a small part of the shrinkList function in Haskell.

For the record, here’s the complete shrinkList from QuickCheck 2.8.2:

-- Shrinks a list of values given a shrinking function for individual values.
shrinkList :: (a -> [a]) -> [a] -> [[a]]
shrinkList shr xs =
  concat [ removes k n xs | k <- takeWhile (>0) (iterate (`div`2) n) ] ++ shrinkOne xs

 where
  n = length xs

  -- The F# version is based only on this function below:
  shrinkOne []       = []
  shrinkOne (x : xs) = [ x' : xs  | x'  <-       shr  x ]
                    ++ [ x  : xs' | xs' <- shrinkOne xs ]

  removes k n xs
    | k > n     = []
    | null xs2  = [[]]
    | otherwise = xs2 : map (xs1 ++) (removes k (n - k) xs2)
   where
    xs1 = take k xs
    xs2 = drop k xs

Hopefully, the next post(s) will become more interesting where I’ll be gluing together some generators, shrinkers, and properties.

Creating F# lists with AutoFixture

Apr 3, 2016

This post explains how to customize AutoFixture in order to work with F# lists.

Problem

An exception is thrown when requesting F# lists with AutoFixture:

Fixture().Create<int list>()

(* ObjectCreationException: AutoFixture was unable to create an instance
 * of type [..] because the traversed object graph contains a circular
 * reference.
 *     Path:
 *       Microsoft.FSharp.Collections.FSharpList`1[System.Int32] tail --> 
 *       Microsoft.FSharp.Collections.FSharpList`1[System.Int32] --> 
 *       Microsoft.FSharp.Collections.FSharpList`1[System.Int32]
 *)

Diagnosis

Lists, and other collection types in the System.Collections.Generic namespace, can be filled via the constructor that takes an IEnumerable<T> as a parameter.

AutoFixture creates such instances via the constructor with the less number of parameters1.

F# lists and the collection types in the System.Collections.Generic namespace are different. One of the differences is the way they’re created:

  • F# lists can be built using the functions in the List module.
  • Collection types in the System.Collections.Generic namespace can be built via the aforementioned constructor(s).

Customize AutoFixture to work with F# lists

The following customization can be applied to a Fixture instance, in order to support the creation of F# lists:

module TestConventions

open System
open Ploeh.AutoFixture
open Ploeh.AutoFixture.Kernel

let (|List|_|) candidate = 
    match candidate |> box with
    | :? Type as t when t.IsGenericType &&
                        t.GetGenericTypeDefinition() = typedefof<list<_>>
        -> Some <| List(t.GetGenericArguments().[0])
    | _ -> None

type ReflectiveList =
    static member Build<'a>(args : obj list) = 
        [ for a in args do
                yield a :?> 'a ]
    static member BuildTyped t args = 
        typeof<ReflectiveList>
            .GetMethod("Build")
            .MakeGenericMethod([| t |])
            .Invoke(null, [| args |])

let listBuilder (f : IFixture) = 
    { new ISpecimenBuilder with
            member this.Create(request, ctx) = 
                match request, ctx with
                | List t, _ ->
                    [ for i in 1..f.RepeatCount -> ctx.Resolve t ]
                    |> ReflectiveList.BuildTyped t
                | _ -> box <| NoSpecimen() }

[<Sealed>]
type ListCustomization() = 
    interface ICustomization with
        member this.Customize fixture =
            fixture.Customizations.Add <| listBuilder fixture

Typical usage

let fixture = Fixture().Customize(ListCustomization())

let listOfInts = fixture.Create<int list>()
(* Length = 3
 *     [0]: 221.0
 *     [1]: 207.0
 *     [2]: 129.0
 *)

let listOfStrings = fixture.Create<string list>()
(* Length = 3
 *     [0]: "224f149d-502d-4387-9203-b5e8a7b4e208"
 *     [1]: "4f2503f4-9bbe-4dd5-ad69-f0e482a41b45"
 *     [2]: "d973a186-ed30-4c0b-abfa-addc1ac7cc46"
 *)

Declarative usage

The above can also be written declaratively using AutoData theories. Here’s an example for xUnit.net:

open Xunit.Extensions
open Ploeh.AutoFixture.Xunit

[<Sealed>]
type TestConventionsAttribute() =
    inherit AutoDataAttribute(
        Fixture().Customize(ListCustomization()))

[<Theory; TestConventions>]
let ``Request a list of ints`` (xs : int list) = 
    (* Length = 3
     *     [0]: 234
     *     [1]: 245
     *     [2]: 3
     *)
    ()

[<Theory; TestConventions>]
let ``Request a list of strings`` (xs : string list) = 
    (* Length = 3
     *     [0]: "ea2a2310-84dc-46e1-aa58-850c57175765"
     *     [1]: "69d4222b-c272-48e9-871c-a4b2715e1945"
     *     [2]: "58ba2b15-b33f-46b8-af91-a50f915c3581"
     *)
    ()

Credits

  • The fact that AutoFixture can’t currently create F# lists out of the box was put to my attention by Rune Ibsen.
  • The customization in this post is based on a similar one that Rune Ibsen showed me.
  • The ReflectiveList code is adapted from this snippet by Rick Minerich.

  1. This strategy can be overridden.

subscribe via RSS