FsCheck


Model-based Testing

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

1: 
2: 
3: 
4: 
5: 
6: 
7: 
type Counter() =
  let mutable n = 0
  member __.Inc() = n <- n + 1
  member __.Dec() = if n > 2 then n <- n - 2 else n <- n - 1
  member __.Get = n
  member __.Reset() = n <- 0
  override __.ToString() = sprintf "Counter=%i" n

We'll elide the class definition in C#, it's very similar.

As a model to test this class we can use an int value which is an abstraction of the object's internal state. The idea is that each operation on the class (in this case, Inc and Dec) affects both the model and the actual object, and after each such operation, the model and the actual instance should still be equivalent.

With this idea in mind, you can write a specification of the Counter class using an int model as follows (full example in C# below):

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
let spec =
  let inc = { new Command<Counter, int>() with
                    override __.RunActual counter = counter.Inc(); counter
                    override __.RunModel m = m + 1
                    override __.Post(counter, m) = counter.Get = m |@ sprintf "model: %i <> %A" m counter
                    override __.ToString() = "inc" }
                           
  let dec = { new Command<Counter, int>() with
                    override __.RunActual counter = counter.Dec(); counter
                    override __.RunModel m = m - 1
                    override __.Post(counter, m) = counter.Get = m |@ sprintf "model: %i <> %A" m counter
                    override __.ToString() = "dec" }
  
  { new ICommandGenerator<Counter,int> with
      member __.InitialActual = Counter()
      member __.InitialModel = 0
      member __.Next model = Gen.elements [inc;dec] }

A specification is put together for FsCheck as an object that implementents ICommandGenerator<'typeUnderTest,'modelType>. It should return an initial object and an initial model of that object; and it should return a generator of Command objects.

Each Command 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 can assert preconditions that need to hold before executing the command: FsCheck will not execute that command if the precondition does 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:

1: 
Check.Quick (Command.toProperty spec)
Falsifiable, after 4 tests (1 shrink) (StdGen (806468692,296584891)):
Label of failing property: model: 2 <> Counter=1
Original:
[inc; inc; inc; dec; dec]
Shrunk:
[inc; inc; inc; dec]

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

Finally, in C#, all this looks as follows:

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 
23: 
24: 
25: 
26: 
27: 
28: 
29: 
30: 
31: 
32: 
33: 
34: 
35: 
36: 
37: 
38: 
39: 
40: 
41: 
42: 
43: 
44: 
45: 
46: 
47: 
48: 
public class CounterSpec : ICommandGenerator<Counter, int> {

    public Gen<Command<Counter, int>> Next(int value) {
        return Gen.Elements(new Command<Counter, int>[] { new Inc(), new Dec() });
    }

    public Counter InitialActual { get { return new Counter(); } }

    public int InitialModel { get { return 0; } }

    private class Inc : Command<Counter,int> {
        public override Counter RunActual(Counter c) {
            c.Inc();
            return c;
        }

        public override int RunModel(int m) {
            return m + 1;
        }

        public override Property Post(Counter c, int m) {
            return (m == c.Get()).ToProperty();
        }

        public override string ToString() {
            return "inc";
        }
    }

    private class Dec : Command<Counter,int>{
        public override Counter RunActual(Counter c) {
            c.Dec();
            return c;
        }

        public override int RunModel(int m) {
            return m - 1;
        }

        public override Property Post(Counter c, int m) {
            return (m == c.Get()).ToProperty();
        }

        public override string ToString() {
            return "dec";
        }
    }
}

And to run:

1: 
2: 
3: 
new CounterSpec()
    .ToProperty()
    .QuickCheck();
namespace FsCheck
namespace System
Multiple items
type Counter =
  new : unit -> Counter
  member Dec : unit -> unit
  member Inc : unit -> unit
  member Reset : unit -> unit
  override ToString : unit -> string
  member Get : int

--------------------
new : unit -> Counter
val mutable n : int
val __ : Counter
val sprintf : format:Printf.StringFormat<'T> -> 'T
val spec : ICommandGenerator<Counter,int>
val inc : Command<Counter,int>
Multiple items
module Command

from FsCheck

--------------------
type Command<'Actual,'Model> =
  new : unit -> Command<'Actual,'Model>
  abstract member Post : 'Actual * 'Model -> Property
  abstract member Pre : 'Model -> bool
  abstract member RunActual : 'Actual -> 'Actual
  abstract member RunModel : 'Model -> 'Model
  override Post : 'Actual * 'Model -> Property
  override Pre : 'Model -> bool

--------------------
new : unit -> Command<'Actual,'Model>
Multiple items
val int : value:'T -> int (requires member op_Explicit)

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

--------------------
type int<'Measure> = int
val counter : Counter
member Counter.Inc : unit -> unit
val __ : Command<Counter,int>
abstract member Command.RunModel : 'Model -> 'Model
val m : int
override Command.Post : 'Actual * 'Model -> Property
property Counter.Get: int
Object.ToString() : string
val dec : Command<Counter,int>
member Counter.Dec : unit -> unit
type ICommandGenerator<'Actual,'Model> =
  interface
    abstract member Next : 'Model -> Gen<Command<'Actual,'Model>>
    abstract member InitialActual : 'Actual
    abstract member InitialModel : 'Model
  end
val __ : ICommandGenerator<Counter,int>
property ICommandGenerator.InitialModel: int
abstract member ICommandGenerator.Next : 'Model -> Gen<Command<'Actual,'Model>>
val model : int
Multiple items
module Gen

from FsCheck

--------------------
type Gen<'a> =
  private | Gen of (int -> StdGen -> 'a)
    interface IGen
    member private Map : f:('a -> 'b) -> Gen<'b>
    static member ( >>= ) : m:Gen<'a1> * k:('a1 -> Gen<'a2>) -> Gen<'a2>
    static member ( <!> ) : f:('a1 -> 'a2) * a:Gen<'a1> -> Gen<'a2>
    static member ( <*> ) : f:Gen<('a1 -> 'a2)> * a:Gen<'a1> -> Gen<'a2>
val elements : xs:seq<'b> -> Gen<'b>
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 toProperty : spec:ICommandGenerator<'Actual,'Model> -> Property
Fork me on GitHub