QuickStart

A Simple Example
A simple example of a property definition is

let prop_RevRev xs = List.rev(List.rev xs) = xs

This property asserts that the reverse of the reverse of a list is the list itself. To check the property, we load this definition in F# interactive and then invoke

> quickCheck prop_RevRev;;
Ok, passed 100 tests.
val it : unit = ()

When a property fails, FsCheck displays a counter-example. For example, if we define

let prop_RevId (xs:list<int>) = List.rev xs = xs

then checking it results in

> quickCheck prop_RevId;;
RevId-Falsifiable, after 3 tests (1 shrink):
[0; 1]
val it : unit = ()


Since v0.4, FsCheck also shrinks the counter example, so that it is the minimal counter example that still fails the test case. In the example above, we see that the counter example is indeed minimal: the list must have at least two different elements. FsCheck also displays how many times it found a smaller (in some way) counter example and so proceeded to shrink further.

Using FsCheck

To use FsCheck, you download the latest FsCheck source or binary. Build and reference the assembly in any projects containing specifications or test data generators. You can then test properties by loading the module they are defined in into F# interactive, and calling

quickCheck <property_name>;; 

or by running and writing a small console application that calls the quickCheck function.

Grouping properties

Usually, you'll write more than one property to test. FsCheck allows you to group together properties as static members of a class:

type ListProperties =
    static member RevRev xs = prop_RevRev xs
    static member RevId xs = prop_RevId xs

These can be checked at once using the quickCheckAll function:

> quickCheckAll (typeof<ListProperties>);;
ListProperties.RevRev-Ok, passed 100 tests.
ListProperties.RevId-Falsifiable, after 2 tests (1 shrink):
[1; 0]

FsCheck now also prints the name of each test.

Since all top level functions of a a module are also compiled as static member of a class with the name of the module, you can also use quickCheck to test all the top level functions in a certain module. However, the type of a module is not directly accessible via F#, so you can use the following trick:

> quickCheck (typeof<ListProperties>.DeclaringType);;
FSI_0016.prop_RevRev-Ok, passed 100 tests.
FSI_0016.prop_RevId-Falsifiable, after 5 tests(1 shrink):
[1; 0]


What do I do if a test loops or encounters an error?

In this case we know that the property does not hold, but quickCheck does not display the counter-example. There is another testing function provided for this situation. Repeat the test using

verboseCheck <property_name>

which displays each test case before running the test: the last test case displayed is thus the one in which the loop or error arises. verboseCheck can also be used with types and modules to check entire groups of properties verbosely.

Caveat
The property above (the reverse of the reverse of a list is the list itself) is not always correct. Consider a list of floats that contains infinity, or nan (not a number). Since infinity <> infinity, and nan <> nan, the reverse of the reverse of [nan,nan] is not actually equal to [nan,nan] if you use straightforward element by element comparison. FsCheck has a knack for finding this kind of specification problem. However, since this behavior is seldom what you want, FsCheck only generates values that are 'neatly' comparable when you leave the type polymorphic (currently, unit, bool, char and string values). To see this error in action, force FsCheck to generate lists of floats:

let prop_RevRevFloat (xs:list<float>) = List.rev(List.rev xs) = xs
> quickCheck prop_RevRevFloat;;
Falsifiable, after 26 tests (3 shrinks):
[nan]

Properties

Properties are expressed as F# function definitions (in the documentation, we give them names beginning with prop_, but this is not necessary).

Properties are universally quantified over their parameters, so

let prop_RevRev xs = List.rev(List.rev xs) = xs

means that the equality holds for all lists xs.

Properties must not have monomorphic types. (Note to QuickCheck users: in QuickCheck, they do.)
`Polymorphic' properties, such as the one above will be tested by FsCheck as if the generic arguments are of type object; this means, that values of various simple types (bool, char, string,...) are generated. It may even be the case that one generated list contains more than one type, e.g. ['r', "1a", true] would be a list that can be used to check the property above.

The generated values are based on the type however, so you may change this behavior simply by giving xs a different inferred or explicit type:

let prop_RevRevInt (xs:list<int>) = List.rev(List.rev xs) = xs

is only checked with lists of int.

The result type of a property should be bool, or Lazy<bool>, or the FsCheck provided type Property.

Conditional Properties

Properties may take the form
<condition> ==> <property>

For example,

let rec ordered xs = 
    match xs with
         | [] -> true
         | [x] -> true
         | x::y::ys ->  (x <= y) && ordered (y::ys)
let rec insert x xs = 
     match xs with
         | [] -> [x]
         | c::cs -> if x <= c then x::xs else c::(insert x cs)                  
let prop_Insert (x:int) xs = ordered xs ==> (ordered (insert x xs))

Such a property holds if the property after ==> holds whenever the condition does.

Testing discards test cases which do not satisfy the condition. Test case generation continues until 100 cases which do satisfy the condition have been found, or until an overall limit on the number of test cases is reached (to avoid looping if the condition never holds). In this case a message such as

Arguments exhausted after 97 tests. 

indicates that 97 test cases satisfying the condition were found, and that the property held in those 97 cases.

Notice that in this case the generated values had to be restricted to int. This is because the generated values need to be comparable, but this is not reflected in the types. Therefore, without the explicit restriction, FsCheck could generate lists containing different types (subtypes of objects), and these are not mutually comparable.

Lazy Properties

Since F# has eager evaluation by default, the above property does more work than necessary: it evaluates the property at the right of the condition no matter what the outcome of the condition on the left. While only a performance consideration in the above example, this may limit the expressiveness of properties - consider:

let prop_Eager a = a <> 0 ==> (1/a = 1/a)
> quickCheck prop_Eager;;
-Falsifiable, after 1 tests: 
0
 with exception:
System.DivideByZeroException: Attempted to divide by zero.

FsCheck needs the F# keyword lazy to force the lazy evaluation of the condition:

let prop_Lazy a = a <> 0 ==> (lazy (1/a = 1/a))
> quickCheck prop_Lazy;;
-Ok, passed 100 tests.

Works as expected.

Quantified Properties

Properties may take the form
forAll <generator> (fun <pattern> -> <property>)

For example,

let prop_InsertWithGen x = forAll orderedList (fun xs -> (ordered (insert x xs)))

The first argument of forAll is a test data generator; by supplying a custom generator, instead of using the default generator for that type, it is possible to control the distribution of test data. In the example, by supplying a custom generator for ordered lists, rather than filtering out test cases which are not ordered, we guarantee that 100 test cases can be generated without reaching the overall limit on test cases. Combinators for defining generators are described later.

There is also:
forAllShrink <generator> <shrinker> (fun <pattern> -> property)

which allows to define a custom generator along with a custom shrink function. A shrink function for values of type 'a is of the form 'a -> seq<'a>. Given a value, it produces the immediate shrinks (i.e. smaller values) of the given value. The sequence should preferably be evaluated lazily, should never contain the value itself, and should return shrinks in order of preference (i.e. smaller values first). For example, the shrinking function for option values is:

let shrink o =
                match o with
                | Some x -> seq { yield None; for x' in shrink x -> Some x' }
                | None  -> Seq.empty

which tries to shrink an option value to None if it isn't already; then if that doesn't work, the values contained in Some x are shrinked. None itself is not shrinked further. Please look in the Arbitrary.fs source file for additional examples of shrinking functions.

Expecting Exceptions

You may want to test that a function or method throws an exception under certain circumstances. The following combinator helps:
throws<'e :> exn,'a> Lazy<'a>

For example,

let prop_ExpectException() = throws<DivideByZeroException,_> (lazy (raise <| DivideByZeroException()))
> quickCheck prop_ExpectException;;
Ok, passed 100 tests.


Timed Properties

Properties may take the form
within <timeout in ms> <Lazy<property>>

For example,

let prop_timeout (a:int) = 
    lazy
        if a>10 then
            while true do Thread.Sleep(1000)
            true
        else 
            true
    |> within 2000

produces:

> quickCheck prop_timeout;;
Timeout of 2 seconds exceeded, after 44 tests (0 shrinks):
12

The first argument is the maximal time the lazy property given may run. If it runs longer, FsCheck considers the test as failed. Otherwise, the outcome of the lazy property is the outcome of within. Note that, although within attempts to cancel the thread in which the property is executed, that may not succeed, and so the thread may actually continue to run until the process ends.

Observing Test Case Distribution

It is important to be aware of the distribution of test cases: if test data is not well distributed then conclusions drawn from the test results may be invalid. In particular, the ==> operator can skew the distribution of test data badly, since only test data which satisfies the given condition is used.

FsCheck provides several ways to observe the distribution of test data. Code for making observations is incorporated into the statement of properties, each time the property is actually tested the observation is made, and the collected observations are then summarized when testing is complete.

Counting Trivial Cases

A property may take the form
trivial <condition> <property>

For example,
let prop_InsertTrivial (x:int) xs = 
    ordered xs ==> (ordered (insert x xs))
    |> trivial (List.length xs = 0)

Test cases for which the condition is true are classified as trivial, and the proportion of trivial test cases in the total is reported. In this example, testing produces

> quickCheck prop_InsertTrivial;;
Ok, passed 100 tests (46% trivial).


Classifying Test Cases

A property may take the form
classify <condition> <string> <property>

For example,

let prop_InsertClassify (x:int) xs = 
    ordered xs ==> (ordered (insert x xs))
    |> classify (ordered (x::xs)) "at-head"
    |> classify (ordered (xs @ [x])) "at-tail"

Test cases satisfying the condition are assigned the classification given, and the distribution of classifications is reported after testing. In this case the result is

> quickCheck prop_InsertClassify;;
-Ok, passed 100 tests.
52% at-tail, at-head.
22% at-tail.
22% at-head.

Note that a test case may fall into more than one classification.

Collecting Data Values

A property may take the form
collect <expression> <property>

For example,

let prop_InsertCollect (x:int) xs = 
    ordered xs ==> (ordered (insert x xs))
        |> collect (List.length xs) 

The argument of collect is evaluated in each test case, and the distribution of values is reported. The type of this argument is printed using any_to_string. In the example above, the output is

> quickCheck prop_InsertCollect;;
-Ok, passed 100 tests.
44% 0.
29% 1.
15% 2.
10% 3.
1% 8.


Combining Observations

The observations described here may be combined in any way. All the observations of each test case are combined, and the distribution of these combinations is reported. For example, testing the property

let prop_InsertCombined (x:int) xs = 
    ordered xs ==> (ordered (insert x xs))
        |> classify (ordered (x::xs)) "at-head"
        |> classify (ordered (xs @ [x])) "at-tail"
        |> collect (List.length xs)

produces

> quickCheck prop_InsertCombined;;
-Arguments exhausted after 97 tests.
32% 0, at-tail, at-head.
14% 1, at-tail.
12% 1, at-head.
9% 2, at-tail.
7% 2, at-head.
5% 2, at-tail, at-head.
5% 1, at-tail, at-head.
3% 3.
3% 2.
2% 4.
2% 3, at-tail.
2% 3, at-head.
1% 5, at-tail.

from which we see that insertion at the beginning or end of a list has not been tested for lists of four elements.

And, Or and Labelling Subproperties

Properties may take the form
<property> .&. <property>
<property> .|. <property>

p1.&. p2 succeeds if both succeed, fails if one of the properties fails, and is rejected when both are rejected.

p1 .|. p2 succeeds if either property succeeds, fails if both properties fail, and is rejected when both are rejected.

The .&. combinator is most commonly used to write complex properties which share a generator. In that case, it might be difficult upon failure to know excatly which sub-property has caused the failure. That's why you can label sub-properties, and FsCheck shows the labels of the failed subproperties when it finds a counter-example. This takes the form:

<string> @| <property>
<property> |@ <string>

For example,

let complexProp (m: int) (n: int) =
  let res = n + m
  (res >= m)    |@ "result > #1" .&.
  (res >= n)    |@ "result > #2" .&.
  (res < m + n) |@ "result not sum"

produces:

>quickCheck complexProp;;
Falsifiable, after 1 test (0 shrinks):
Label of failing property: result not sum
0
0


It's perfectly fine to apply more than one label to a property; FsCheck displays all the applicable labels. This is useful for displaying intermediate results, for example:

let propMul (n: int, m: int) =
  let res = n*m
  sprintf "evidence = %i" res @| (
    "div1" @| (m <> 0 ==> lazy (res / m = n)),
    "div2" @| (n <> 0 ==> lazy (res / n = m)),
    "lt1"  @| (res > m),
    "lt2"  @| (res > n))
> quickCheck propMul;;
Examples.propMul-Falsifiable, after 1 test (0 shrinks):
Labels of failing property: evidence = 0, lt1
(0, 0)


Notice that the above property combines subproperties by tupling them. This works for tuples up to length 6. It also works for lists. In general form

(<property1>,<property2>,...,<property6>) means <property1> .&. <property2> .&.... .&.<property6>
[property1;property2,...,propertyN] means <property1> .&. <property2> .&.... .&.<propertyN>

The example written as a list:

let propMulList (n: int, m: int) =
  let res = n*m
  sprintf "evidence = %i" res @| [
    "div1" @| (m <> 0 ==> lazy (res / m = n));
    "div2" @| (n <> 0 ==> lazy (res / n = m));
    "lt1"  @| (res > m);
    "lt2"  @| (res > n)]

produces the exact same result.

Test Data Generators: The Type Gen

Test data is produced by test data generators. FsCheck defines default generators for some often used types, but you can use your own, and will need to define your own generators for any new types you introduce.

Generators have types of the form Gen<'a>; this is a generator for values of type a. For manipulating values of type Gen, a computation expression called gen is provided by FsCheck.

Generators are built up on top of the function

val choose : (int * int -> int Gen)

which makes a random choice of a value from an interval, with a uniform distribution. For example, to make a random choice between the elements of a list, use

let chooseFromList xs = gen { let! i = choose (0, List.length xs-1) 
                              return (List.nth xs i) }

Choosing Between Alternatives

A generator may take the form
oneof <list of generators>

which chooses among the generators in the list with equal probability. For example,

oneof [ gen { return true }; gen { return false } ]

generates a random boolean which is true with probability one half.

We can control the distribution of results using the function

val frequency: (int * 'a Gen) list -> 'a Gen 

instead. Frequency chooses a generator from the list randomly, but weights the probability of choosing each alternative by the factor given. For example,

frequency [ (2, gen { return true }); (1, gen { return false })]

generates true two thirds of the time.

The Size of Test Data

Test data generators have an implicit size parameter; FsCheck begins by generating small test cases, and gradually increases the size as testing progresses. Different test data generators interpret the size parameter in different ways: some ignore it, while the list generator, for example, interprets it as an upper bound on the length of generated lists. You are free to use it as you wish to control your own test data generators.

You can obtain the value of the size parameter using

val sized : ((int -> 'a Gen) -> 'a Gen)

sized g calls g, passing it the current size as a parameter. For example, to generate natural numbers in the range 0 to size, use

sized <| fun s -> choose (0,s)

The purpose of size control is to ensure that test cases are large enough to reveal errors, while remaining small enough to test fast. Sometimes the default size control does not achieve this. For example, towards the end of a test run arbitrary lists may have up to 50 elements, so arbitrary lists of lists may have up to 2500, which is too large for efficient testing. In such cases it can be useful to modify the size parameter explicitly. You can do so using

val resize : (int -> 'a Gen -> 'a Gen)

resize n g invokes generator g with size parameter n. The size parameter should never be negative. For example, to generate a random matrix it might be appropriate to take the square root of the original size:

let matrix gn = sized <| fun s -> resize (s|>float|>sqrt|>int) gn

Generating Recursive Data Types

Generators for recursive data types are easy to express using oneof or frequency to choose between constructors, and F#'s standard computation expression syntax to form a generator for each case. There are also liftGen functions for arity up to 6 to lift constructors and functions into the Gen type. For example, if the type of trees is defined by

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

then a generator for trees might be defined by

let rec unsafeTree() = 
    oneof [ liftGen (Leaf) arbitrary; 
            liftGen2 (fun x y -> Branch (x,y)) (unsafeTree()) (unsafeTree())]

However, a recursive generator like this may fail to terminate with a StackOverflowException, or produce very large results. To avoid this, recursive generators should always use the size control mechanism. For example,

let private tree =
    let rec tree' s = 
        match s with
            | 0 -> liftGen (Leaf) arbitrary
            | n when n>0 -> 
            let subtree() = tree' (n/2)
            oneof [ liftGen (Leaf) arbitrary; 
                    liftGen2 (fun x y -> Branch (x,y)) (subtree()) (subtree())]
            | _ -> raise(ArgumentException"Only positive arguments are allowed")
    sized tree'

Note that
  • We guarantee termination by forcing the result to be a leaf when the size is zero.
  • We halve the size at each recursion, so that the size gives an upper bound on the number of nodes in the tree. We are free to interpret the size as we will.
  • The fact that we share the subtree generator between the two branches of a Branch does not, of course, mean that we generate the same tree in each case.

Useful Generator Combinators

If g is a generator for type t, then
two g generates a pair of t's,
three g generates a triple of t's,
four g generates a quadruple of t's,
If xs is a list, then elements xs generates an arbitrary element of xs.
vectorOf n g generates a list of exactly n t's.
listOf g generates a lis of t's whose length is determined by the size parameter
nonEmptyListOf g generates a non-empty list of t's.
constant v generates the value v.
suchThat p g generates t's that satisfy the predicate p. Make sure there is a high chance that the predicate is satisfied.
suchThatOption p g generates Some t's that satisfy the predicate p, and None if none are found. (After "trying hard")

Generating random function values

Perhaps surprisingly, FsCheck can generate random functions.

To generate random functions of type 'a->'b, you need to provide an instance of type 'a-> 'b Gen -> 'b Gen, which we'll call the cogenerator. The implementation of ('a->'b) Gen uses a cogenerator for type a. If you only want to generate random values of a type, you need only to define a generator for that type, while if you want to generate random functions over the type also, then you should define a cogenerator as well.

A cogenerator function interprets a value of type a as a generator transformer. It should be defined so that different values are interpreted as independent generator transformers. These can be programmed using the function

val variant : (int -> 'a Gen -> 'a Gen)

For different natural numbers i and j, variant i g and variant j g are independent generator transformers. The argument of variant must be non-negative, and, for efficiency, should be small. Cogenerators can be defined by composing together generator transformers constructed with variant.

An intuitive way to think about this, is that a generator can generate a value of a certain type based on a random int (provided maybe by choose), while a cogenerator maps the value back onto that int.

For example,for the type Tree defined above, a suitable instance of a cogenerator, allowing you to define functions Tree -> 'a, can be defined as follows

let rec private cotree t = 
    match t with
       | (Leaf n) -> variant 0 << coarbitrary n
       | (Branch (t1,t2)) -> variant 1 << cotree t1 << cotree t2

Default Generators based on type

FsCheck defines default test data generators for some often used types: unit, bool, int, float, char, string, tuples up to length 6, lists, arrays, objects and functions. Furthermore, by using reflection, FsCheck can derive default implementations of record types, discriminated unions and arrays in terms of any primitive types that are defined (either in FsCheck or by you).

You do not need to define these generators explicity for every property: FsCheck can provide a property with appropriate generators for all of the property's arguments, if it knows them or can derive them. Usually you can let type inference do the job of finding out these types based on your properties. However if you want to coerce FsCheck to use a particular generator, you can do so by providing the appropriate type annotations.

You can tell FsCheck about generators for your own types, by defining static members of a class, each of which should return an instance of a subclass of the class Arbitrary<'a>:

type MyGenerators =
    static member Tree() =
        {new Arbitrary<Tree>() with
            override x.Arbitrary = tree
            override x.CoArbitrary t = cotree t }

Replace the 'a by the particular type you are defiing a generator for. Only the Arbitrary method needs to be defined; CoArbitrary will fail by default if a function is generated with the type as domain, and Shrink by default returns the empty sequence (i.e. no shrinking will occur for this type).

Now, to register all generators in this class:

registerGenerators<MyGenerators>()

FsCheck now knows about Tree types, and can not only generate Tree values, but also lists, tuples and option values containing Trees:

let prop_RevRevTree (xs:list<Tree>) = List.rev(List.rev xs) = xs
> quickCheck prop_RevRevTree;;
-Ok, passed 100 tests.

To generate types with a generic type argument, e.g.:

type Box<'a> = Whitebox of 'a | Blackbox of 'a

you can use the same principle. So the class MyGenerators can be writtten as follows:

let boxgen() = 
    gen {   let! a = arbitrary
            return! elements [ Whitebox a; Blackbox a] }

type MyGenerators =
    static member Tree() =
        {new Arbitrary<Tree>() with
            override x.Arbitrary = tree
            override x.CoArbitrary t = cotree t }
    static member Box() = 
        {new Arbitrary<Box<'a>>() with
            override x.Arbitrary = boxgen() }

Notice that we use the function 'val arbitrary<'a> : Gen<'a>' to get the generator for the type argument of Box. This allows you to define generators recursively. Similarly, there is a function coarbitrary and shrink. Look at the FsCheck source for examples of default Arbitrary implementations to get a feeling of how to write such generators.

Now, the following property can be checked (a collect is added to view some of the generated values):

let prop_RevRevBox (xs:list<Box<int>>) = List.rev(List.rev xs) = xs |> collect xs
quickCheck prop_RevRevBox;;
-Ok, passed 100 tests.
15% [].
3% [Whitebox 0].
3% [Blackbox -1].
2% [Whitebox -2].
2% [Blackbox 0].
2% [Blackbox -2].
1% [Whitebox 7; Blackbox 12].
1% [Whitebox 6; Whitebox -3; Whitebox 1; Whitebox 8; Whitebox 13; Whitebox 14;
 Blackbox 4; Whitebox -15; Whitebox -12; Whitebox -14; Blackbox 15; Whitebox 10;
 Whitebox 0; Whitebox -10].
...

Note that the class needs not be tagged with attributes in any way. FsCheck determines the type of the generator by the return type of each static member,

You cannot register the same type multiple times; FsCheck throws an exception if you try. There is however an overwriteGenerators function that does allow this.

Polymorphic properties

It was shown already that FsCheck can handle polymorphic properties, like:

let prop_RevRev xs = List.rev(List.rev xs) = xs

FsCheck handles these by interpreting the type argument as if of type obj. The generator for object currently generates random values of type unit, bool, char and string. So, checking the property above:

> verboseCheck prop_RevRev;;
0:
[|[]|]
1:
[|["oY"]|]
2:
[|['N'; '\012']|]
3:
[|[null; "mP"; ""]|]
4:
[|[]|]
5:
[|[true; true; true; "\022?"]|]
6:
[|[';']|]
...

Note that each generated list is not monomorphic, as you might expect.

Stateful Testing

FsCheck also allows you to test objects, which usually encapsulate internal state through a set of methods. FsCheck, through a very small extension, allows you to do model-based specification of a class under test. Consider the following class, with an artificial bug in it:

type Counter() =
  let mutable n = 0
  member x.Inc() = n <- n + 1
  member x.Dec() = if n > 2 then n <- n - 2 else n <- n - 1
  member x.Get = n
  member x.Reset() = n <- 0
  override x.ToString() = n.ToString()

The obvious model to test this class is just an int value which will serve as an abstraction of the object's internal state. With this idea in mind, you can write a specification as follows:

let spec =
    let inc = 
        { new ICommand<Counter,int>() with
            member x.RunActual c = c.Inc(); c
            member x.RunModel m = m + 1
            member x.Post (c,m) = m = c.Get 
            override x.ToString() = "inc"}
    let dec = 
        { new ICommand<Counter,int>() with
            member x.RunActual c = c.Dec(); c
            member x.RunModel m = m - 1
            member x.Post (c,m) = m = c.Get 
            override x.ToString() = "dec"}
    { new ISpecification<Counter,int> with
        member x.Initial() = (new Counter(),0)
        member x.GenCommand _ = elements [inc;dec] }

A specification is an object that Implementents ISpecification<'typeUnderTest,'modelType>. It should return an initial object and an initial model of that object; and it should return a generator of ICommand objects.

Each ICommand object typically represents one method to call on the object under test, and describes what happens to the model and the object when the command is executed. Also, it asserts preconditions that need to hold before executing the command: FsCheck will not execute that command if the precondittion doesn not hold. It asserts postconditions that should hold after a command is executed: FsCheck fails the test if a postcondition does not hold.

Preferably also override ToString in each command so that counterexamples can be printed.

A specification can be checked as follows:

quickCheckN "Counter" (fun () -> asProperty spec)
Counter-Falsifiable, after 26 tests (5 shrinks):
null
[inc; inc; inc; dec]

Notice that not only has FsCheck found our "bug", it has also produced the minimal sequence that leads to it.

Properties of Functions

Since FsCheck can generate random function values, it can check properties of functions. For example, we can check associativity of function composition as follows:

let rec cotree t = 
    match t with
       | (Leaf n) -> variant 0 << coarbitrary n
       | (Branch (t1,t2)) -> variant 1 << cotree t1 << cotree t2

let prop_Assoc (x:Tree) (f:Tree->float,g:float->char,h:char->int) = ((f >> g) >> h) x = (f >> (g >> h)) x

where we assume the generator and cogenerator for trees are registered; we thus generate functions Tree -> 'a. If a counter-example is found, function values will be displayed as "<func>".

However, FsCheck can show you the generated function in more detail, by using the Function datatype. For example:

let propMap (Function (_,f)) (l:list<int>) =
    not l.IsEmpty ==>
    lazy (List.map f l = ((*f*)(List.hd l)) :: (List.map f (List.tl l)))
>quickCheck propMap;;
Falsifiable, after 2 tests (3 shrinks):
{-1->0; 0->0; 1->0}
[1]

The type Function<'a,'b> = Function of ref<list<('a'b)>> ('a ->'b) keeps a map internally of all the arguments it was called with, and the result it produced. In your properties, you can extract the actual function by pattern matching as in the example. Function is used to print the function, and is also to shrink it.

Use pattern matching instead of forAll to define custom generators

For example:

type NonNegativeInt = NonNegative of int
type NonZeroInt = NonZero of int
type PositiveInt = Positive of int

type ArbitraryModifiers =
    static member NonNegativeInt() =
        { new Arbitrary<NonNegativeInt>() with
            override x.Arbitrary = arbitrary |> fmapGen (NonNegative << abs)
            override x.CoArbitrary (NonNegative i) = coarbitrary i
            override x.Shrink (NonNegative i) = shrink i |> Seq.filter ((<) 0) |> Seq.map NonNegative }
    static member NonZeroInt() =
        { new Arbitrary<NonZeroInt>() with
            override x.Arbitrary = arbitrary |> suchThat ((<>) 0) |> fmapGen NonZero 
            override x.CoArbitrary (NonZero i) = coarbitrary i
            override x.Shrink (NonZero i) = shrink i |> Seq.filter ((=) 0) |> Seq.map NonZero }
    static member PositiveInt() =
        { new Arbitrary<PositiveInt>() with
            override x.Arbitrary = arbitrary |> suchThat ((<>) 0) |> fmapGen (Positive << abs) 
            override x.CoArbitrary (Positive i) = coarbitrary i
            override x.Shrink (Positive i) = shrink i |> Seq.filter ((<=) 0) |> Seq.map Positive }

registerGenerators<ArbitraryModifiers>()

let prop_NonNeg (NonNegative i) = i >= 0
quickCheckN "NonNeg" prop_NonNeg

let prop_NonZero (NonZero i) = i <> 0
quickCheckN "NonZero" prop_NonZero

let prop_Positive (Positive i) = i > 0
quickCheckN "Pos" prop_Positive

This make properties much more readable, especially since you can define custom shrink functions as well.

Register generators and test, without classes (almost)

Since generators are given as static members of classes, and properties can be grouped together as static members of classes, and since top level let functions are compiled as static member of their enclosing module (which is compiled as a class), you can simply define your properties and generators as top level let-bound functions, and then register all generators and and all properties at once using the following trick:

let myprop =....
let mygen =...
let helper = "returns a string"
let private helper' = true

type Marker = member x.Null = ()
registerGenerators (typeof<Marker>.DeclaringType)
quickCheckAll (typeof<Marker>.DeclaringType)

The Marker type is just any type defined in the module, to be able to get to the module's Type. As far as I know, F# offer no way to get to a module Type directly.

FsCheck determines the intent of the function based on its return type:
  • Properties: return bool, Lazy<bool> or Property
  • Generators: return Gen<_>
All other functions are respectfully ignored. If you have top level functions that return type Gen<_> but do not want them checked or registered, just make them private. FsCheck will ignore those functions.

Implementing IRunner to integrate FsCheck with mb|x|N|cs|...Unit

The Config type that can be passed to the check function takes an IRunner as argument. This interface has two methods:
  • OnArguments is called after every test, passing the implementation the test number, the arguments and the every function.
  • OnShrink is called at every succesful shrink.
  • OnFinished: is called with the name of the test and the outcome of the overall test run. This is used in the example below to call Assert statements from an outside unit testing framework and allows easy integration with a number of unit testing frameworks. You can leverage another unit testing framework's ability to setup and tear down tests, have a nice graphical runner etc.

Also, there is a function testFinishedToString which produces the standard string that FsCheck uses to print counter-examples, i.e. with labels, nicely formatted and with anything else that might be added in the future.

let xUnitRunner = 
    { new IRunner with 
        member x.OnArguments(_,_,_) = ()  
        member x.OnShrink(_,_) = ()
        member x.OnFinished(name, result) = 
            match result with 
                | True data -> Assert.True(true)
                | _ -> Assert.True(false, testFinishedToString name result) 
        } 
        
let config = {quick with Runner = xUnitRunner}

Implementing IRunner to customize printing of generated arguments

By default, FsCheck prints generated arguments using sprintf "%A", or so called structured formatting. This usually does what you expect, i.e. for primitive types the value, for objects the ToString override and so on. Occasionally it happens that this is not what you want. (An interesting motivating case that was reported, is testing with COM objects - overriding ToString is not an option and structured formatting does not do anything useful with it). On one hand you can use the label combinator to solve this on a per property basis, but a more structured solution can be achieved by implementing IRunner. For example:

type Foo = Foo of int
type Bar = Bar of string

let formatter (o:obj) =
    match o with
    | :? Foo as foo -> box "it's a foo"
    | :? Bar as bar -> box "it's a bar"
    | _ -> o

//customizing output of counter-examples etc
let formatterRunner =
    { new IRunner with
        member x.OnArguments (ntest,args, every) =
            printf "%s" (every ntest (args |> List.map formatter))
        member x.OnShrink(args, everyShrink) =
            printf "%s" (everyShrink (args |> List.map formatter))
        member x.OnFinished(name,testResult) = 
            let testResult' = match testResult with 
                                | TestResult.False (testData,origArgs,shrunkArgs,outCome,seed) -> 
                                    TestResult.False (testData,origArgs |> List.map formatter, shrunkArgs |> List.map formatter,outCome,seed)
                                | t -> t
            printf "%s" (testFinishedToString name testResult') 
    }

let formatter_prop (foo:Foo) (bar:Bar) (i:int) = i < 10 //so it takes a while before the fail
check { verbose with Runner = formatterRunner} formatter_prop

which outputs:

0:
"it's a foo"
"it's a bar"
0
1:
"it's a foo"
"it's a bar"
1
(etc)
Falsifiable, after 40 tests (6 shrinks) (StdGen (1013864023,295132170)):
"it's a foo"
"it's a bar"
10

An equality comparison that prints the left and right sides of the equality

A common property is checking for equality. If a test case fails, FsCheck prints the counterexample, but sometimes it is useful to print the left and right side of the comparison as well, especially if you do some complicated calculations with the generated arguments first. Easiest thing is to define your own printing equality combinator:

let (.=.) left right = left = right |@ sprintf "%A = %A" left right

et compare (i:int) (j:int) = 2*i+1  .=. 2*j-1
quickCheck compare

which prints:

Falsifiable, after 1 test (0 shrinks) (StdGen (231038195,295132764)):
Label of failing property: 1 = -1
0
0

OF course, you can do this for any operator or function that you often use.

Some ways to use FsCheck
  1. By adding properties and generators to an fsx file in your assembly. It's easy to execute, just press ctrl-a and alt-enter, and the results are displayed in F# Interactive. Be careful when referencing dlls that are built in your solution; F# Interactive will lock those for the remainder of the session, and you won't be able to build unitl you quit the session. One solution is to include the source files instead of the dlls, but that makes the process slower. Useful for smaller projects. Difficult to debug, as far as I know.
  2. By making a separate console application. Easy to debug, no annoying locks on assemblies. Your best option if you only use FsCheck for testing and your properties span multiple assemblies
  3. By using another unit testing framework. Useful if you have a mixed FsCheck/unit testing approach (some things are easier to check using unit tests, and vice versa), and you like a graphical runner. Depending on what unit testing framework you use, you may get good integration with Visual Studio for free. See also above for ways to customize FsCheck for this scenario.

Last edited Sep 9, 2010 at 3:37 PM by kurt2001, version 6

Comments

No comments yet.