FsCheck


Properties

Properties are expressed as F# function definitions or C# lambdas or methods. Properties are universally quantified over their parameters, so

1: 
let revRevIsOrig (xs:list<int>) = List.rev(List.rev xs) = xs
1: 
2: 
3: 
public static bool RevRevIsOriginal(int[] ts) {
    return ts.Reverse().Reverse().SequenceEqual(ts);
}

means that the equality holds for all lists xs.

Properties must not have generic types - because there can be so many different kinds of constraints on generic types, some of which may not even be visible from the type signature, we currently think allowing FsCheck to generate a generic type is not worth the added complexity. It's very simple to fix any types anyway simply by adding some type annotations.

FsCheck can check properties of various forms - these forms are called testable, and are indicated in the API by a generic type called 'Testable. A 'Testable may be a function of any number of parameters that returns bool or unit. In the latter case, a test passes if it does not throw. The entry point to create properties is the Prop module.

Like all of FsCheck's API, there are C# counterparts for all of the F# methods described.

Conditional Properties

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

For example,

1: 
2: 
let insertKeepsOrder (x:int) xs = ordered xs ==> ordered (insert x xs)
Check.Quick insertKeepsOrder
1: 
2: 
Prop.ForAll<int, int[]>((x, xs) => xs.Insert(x).IsOrdered().When(xs.IsOrdered()))
    .QuickCheck();
Arguments exhausted after 21 tests.

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:

1: 
2: 
let tooEager a = a <> 0 ==> (1/a = 1/a)
Check.Quick tooEager
Falsifiable, after 1 test (0 shrinks) (StdGen (502035714,296521705)):
Original:
0
with exception:
System.DivideByZeroException: Attempted to divide by zero.
   at FSI_0022.tooEager(Int32 a) in C:\Users\Kurt\Projects\FsCheck\FsCheck\input.fsx:line 1
   at FsCheck.Testable.evaluate[a,b](FSharpFunc`2 body, a a)

Non-strict evaluation is needed here to make sure the propery is checked correctly:

1: 
2: 
let moreLazy a = a <> 0 ==> (lazy (1/a = 1/a))
Check.Quick moreLazy
1: 
2: 
Prop.ForAll<int>(a => new Func<bool>(() => 1 / a == 1 / a).When(a != 0))
    .QuickCheck();
Ok, passed 100 tests.

Quantified Properties

Properties may take the form forAll <arbitrary> (fun <args> -> <property>).

For example,

1: 
2: 
3: 
let orderedList = Arb.from<list<int>> |> Arb.mapFilter List.sort ordered
let insertWithArb x = Prop.forAll orderedList (fun xs -> ordered(insert x xs))
Check.Quick insertWithArb
1: 
2: 
3: 
4: 
5: 
var orderedList = Arb.From<int[]>()
                     .MapFilter(xs => xs.OrderBy(i => i).ToArray(), xs => xs.IsOrdered());

Prop.ForAll<int>(x => Prop.ForAll(orderedList, xs => xs.Insert(x).IsOrdered()))
    .QuickCheck();
Ok, passed 100 tests.

The first argument of forAll is an IArbitrary instance. Such an instance encapsulates a test data generator and a shrinker (more on that in Test Data). 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 in Test Data.

Expecting exceptions

You may want to test that a function or method throws an exception under certain circumstances. Use throws<'e :> exn,'a> Lazy<'a> to achieve this. For example:

1: 
2: 
let expectDivideByZero() = Prop.throws<DivideByZeroException,_> (lazy (raise <| DivideByZeroException()))
Check.Quick expectDivideByZero
Ok, passed 100 tests.
1: 
  

This functionality is not available in the C# API.

Timed Properties

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

For example,

1: 
2: 
3: 
4: 
5: 
6: 
7: 
8: 
9: 
let timesOut (a:int) = 
    lazy
        if a>10 then
            do System.Threading.Thread.Sleep(3000)
            true
        else 
            true
    |> Prop.within 1000
Check.Quick timesOut

The first argument is the time the lazy property 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.

This functionality is not available in the C# API.

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,

1: 
2: 
3: 
4: 
let insertTrivial (x:int) xs = 
  ordered xs ==> (ordered (insert x xs))
  |> Prop.trivial (List.length xs = 0)
Check.Quick insertTrivial
1: 
2: 
3: 
4: 
5: 
Prop.ForAll<int, int[]>((x, xs) =>
            xs.Insert(x).IsOrdered()
            .When(xs.IsOrdered())
            .Classify(xs.Count() == 0, "trivial"))
    .QuickCheck();

Test cases for which the condition is true are classified as trivial, and the proportion of trivial test cases in the total is reported:

Arguments exhausted after 14 tests (28% trivial).

Classifying Test Cases

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

For example,

1: 
2: 
3: 
4: 
5: 
let insertClassify (x:int) xs = 
  ordered xs ==> (ordered (insert x xs))
  |> Prop.classify (ordered (x::xs)) "at-head"
  |> Prop.classify (ordered (xs @ [x])) "at-tail"
Check.Quick insertClassify
1: 
2: 
3: 
4: 
5: 
6: 
Prop.ForAll<int, int[]>((x, xs) =>
        xs.Insert(x).IsOrdered()
        .When(xs.IsOrdered())
        .Classify(new[] { x }.Concat(xs).IsOrdered(), "at-head")
        .Classify(xs.Concat(new int[] { x }).IsOrdered(), "at-tail"))
    .QuickCheck();

Test cases satisfying the condition are assigned the classification given, and the distribution of classifications is reported after testing:

Arguments exhausted after 19 tests.
42% at-tail, at-head.
36% at-head.
21% at-tail.

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,

1: 
2: 
3: 
4: 
let insertCollect (x:int) xs = 
  ordered xs ==> (ordered (insert x xs))
      |> Prop.collect (List.length xs)
Check.Quick insertCollect
1: 
2: 
3: 
4: 
5: 
Prop.ForAll<int, int[]>((x, xs) =>
        xs.Insert(x).IsOrdered()
        .When(xs.IsOrdered())
        .Collect("length " + xs.Count().ToString()))
    .QuickCheck();

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 sprintf "%A":

Arguments exhausted after 22 tests.
40% 1.
22% 2.
22% 0.
9% 3.
4% 5.

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:

1: 
2: 
3: 
4: 
5: 
6: 
let insertCombined (x:int) xs = 
    ordered xs ==> (ordered (insert x xs))
    |> Prop.classify (ordered (x::xs)) "at-head"
    |> Prop.classify (ordered (xs @ [x])) "at-tail"
    |> Prop.collect (List.length xs)
Check.Quick insertCombined
1: 
2: 
3: 
4: 
5: 
6: 
7: 
Prop.ForAll<int, int[]>((x, xs) =>
        xs.Insert(x).IsOrdered()
        .When(xs.IsOrdered())
        .Classify(new [] { x }.Concat(xs).IsOrdered(), "at-head")
        .Classify(xs.Concat(new int[] { x }).IsOrdered(), "at-tail")
        .Collect("length " + xs.Count().ToString()))
    .QuickCheck();
Arguments exhausted after 11 tests.
27% 0, at-tail, at-head.
18% 1, at-tail.
18% 1, at-head.
9% 3, at-tail.
9% 3.
9% 2, at-head.
9% 2.

And, Or and Labels

Properties may take the form

  • <property> .&. <property> succeeds if both succeed, fails if one of the properties fails, and is rejected when both are rejected.
  • <property> .|. <property>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 excactly 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> or <property> |@ <string>.

For example,

1: 
2: 
3: 
4: 
5: 
6: 
let complex (m: int) (n: int) =
  let res = n + m
  (res >= m)    |@ "result > #1" .&.
  (res >= n)    |@ "result > #2" .&. 
  (res < m + n) |@ "result not sum"
Check.Quick complex
1: 
2: 
3: 
4: 
5: 
6: 
Prop.ForAll<int, int>((m, n) => {
    var result = m + n;
    return (result >= m).Label("result > #1")
       .And(result >= n).Label("result > #2")
       .And(result < m + n).Label("result not sum");
}).QuickCheck();
Falsifiable, after 1 test (2 shrinks) (StdGen (519666345,296521705)):
Label of failing property: result not sum
Original:
2
2
Shrunk:
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:

1: 
2: 
3: 
4: 
5: 
6: 
7: 
8: 
let multiply (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))
Check.Quick multiply
1: 
2: 
3: 
4: 
5: 
6: 
7: 
8: 
Prop.ForAll<int, int>((n, m) => {
    var res = n * m;
    return (new Func<bool>(() => res / m == n)).When(m != 0.0).Label("div1")
      .And((new Func<bool>(() => res / n == m)).When(n != 0.0).Label("div2"))
      .And((res > m).Label("lt1"))
      .And((res > n).Label("lt2"))
      .Label(string.Format("evidence = {0}", res));
}).QuickCheck();
Falsifiable, after 1 test (0 shrinks) (StdGen (520598537,296521705)):
Labels of failing property (one or more is failing):
evidence = 0
lt1
Original:
(0, 0)

Notice that the above property combines subproperties by tupling them. This works for tuples up to length 6 and lists:

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

The example written as a list:

1: 
2: 
3: 
4: 
5: 
6: 
7: 
let multiplyAsList (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 same result.

namespace FsCheck
namespace System
val revRevIsOrig : xs:int list -> bool
val xs : int list
type 'T list = List<'T>
Multiple items
val int : value:'T -> int (requires member op_Explicit)

--------------------
type int = int32

--------------------
type int<'Measure> = int
Multiple items
module List

from Microsoft.FSharp.Collections

--------------------
type List<'T> =
  | ( [] )
  | ( :: ) of Head: 'T * Tail: 'T list
    interface IReadOnlyCollection<'T>
    interface IEnumerable
    interface IEnumerable<'T>
    member GetSlice : startIndex:int option * endIndex:int option -> 'T list
    member Head : 'T
    member IsEmpty : bool
    member Item : index:int -> 'T with get
    member Length : int
    member Tail : 'T list
    static member Cons : head:'T * tail:'T list -> 'T list
    ...
val rev : list:'T list -> 'T list
val ordered : xs:'a list -> bool (requires comparison)
val xs : 'a list (requires comparison)
val x : 'a (requires comparison)
val y : 'a (requires comparison)
val ys : 'a list (requires comparison)
val insert : x:'a -> xs:'a list -> 'a list (requires comparison)
val c : 'a (requires comparison)
val cs : 'a list (requires comparison)
val insertKeepsOrder : x:int -> xs:int list -> Property
val x : int
type Check =
  static member All : config:Config -> unit
  static member All : config:Config * test:Type -> unit
  static member Method : config:Config * methodInfo:MethodInfo * ?target:obj -> unit
  static member One : config:Config * property:'Testable -> unit
  static member One : name:string * config:Config * property:'Testable -> unit
  static member Quick : property:'Testable -> unit
  static member Quick : name:string * property:'Testable -> unit
  static member QuickAll : unit -> unit
  static member QuickAll : test:Type -> unit
  static member QuickThrowOnFailure : property:'Testable -> unit
  ...
static member Check.Quick : property:'Testable -> unit
static member Check.Quick : name:string * property:'Testable -> unit
val tooEager : a:int -> Property
val a : int
val moreLazy : a:int -> Property
val orderedList : Arbitrary<int list>
module Arb

from FsCheck
val from<'Value> : Arbitrary<'Value>
val mapFilter : mapper:('a -> 'a) -> pred:('a -> bool) -> a:Arbitrary<'a> -> Arbitrary<'a>
val sort : list:'T list -> 'T list (requires comparison)
val insertWithArb : x:int -> Property
module Prop

from FsCheck
val forAll : arb:Arbitrary<'Value> -> body:('Value -> 'Testable) -> Property
val expectDivideByZero : unit -> Property
val throws<'Exception,'Testable (requires 'Exception :> exn)> : p:Lazy<'Testable> -> Property (requires 'Exception :> exn)
Multiple items
type DivideByZeroException =
  inherit ArithmeticException
  new : unit -> DivideByZeroException + 2 overloads

--------------------
DivideByZeroException() : DivideByZeroException
DivideByZeroException(message: string) : DivideByZeroException
DivideByZeroException(message: string, innerException: exn) : DivideByZeroException
val raise : exn:Exception -> 'T
val timesOut : a:int -> Property
namespace System.Threading
Multiple items
type Thread =
  inherit CriticalFinalizerObject
  new : start:ThreadStart -> Thread + 3 overloads
  member Abort : unit -> unit + 1 overload
  member ApartmentState : ApartmentState with get, set
  member CurrentCulture : CultureInfo with get, set
  member CurrentUICulture : CultureInfo with get, set
  member DisableComObjectEagerCleanup : unit -> unit
  member ExecutionContext : ExecutionContext
  member GetApartmentState : unit -> ApartmentState
  member GetCompressedStack : unit -> CompressedStack
  member GetHashCode : unit -> int
  ...

--------------------
Threading.Thread(start: Threading.ThreadStart) : Threading.Thread
Threading.Thread(start: Threading.ParameterizedThreadStart) : Threading.Thread
Threading.Thread(start: Threading.ThreadStart, maxStackSize: int) : Threading.Thread
Threading.Thread(start: Threading.ParameterizedThreadStart, maxStackSize: int) : Threading.Thread
Threading.Thread.Sleep(timeout: TimeSpan) : unit
Threading.Thread.Sleep(millisecondsTimeout: int) : unit
val within : time:int -> lazyProperty:Lazy<'Testable> -> Property
val insertTrivial : x:int -> xs:int list -> Property
val trivial : b:bool -> ('Testable -> Property)
val length : list:'T list -> int
val insertClassify : x:int -> xs:int list -> Property
val classify : b:bool -> name:string -> ('Testable -> Property)
val insertCollect : x:int -> xs:int list -> Property
val collect : v:'CollectedValue -> ('Testable -> Property)
val insertCombined : x:int -> xs:int list -> Property
val complex : m:int -> n:int -> Property
val m : int
val n : int
val res : int
val multiply : n:int * m:int -> Property
val sprintf : format:Printf.StringFormat<'T> -> 'T
val multiplyAsList : n:int * m:int -> Property
Fork me on GitHub