Eric's FsCheck Notes

As I have never used FsCheck before, here are my notes.

FsCheck can be found here. https://github.com/fsharp/FsCheck

We bring in FsCheck using NuGet.

To learn this I started with the Quick Start

To get this first example to work I created a new F# library project using Visual Studio 2012 (VS).
I then used NuGet to install FsCheck. This installed version 0.9.1.0. into the packages directory of the VS project folder.
The first example runs using F# interactive (FSI) which I used from within VS. I type the commands into Script.fsx and then send them to FSI individually.

First I need to verify which directory we are pointing at so FSI can locate files. (Think command line current directory.)

printfn __SOURCE_DIRECTORY__;;  
E:\Projects\Visual Studio 2012\FsCheckLearning001\FsCheckLearning001
val it : unit = ()

Next I needed to tell FSI where to locate FsCheck code relative to the source directory.

#I "./../packages"  
--> Added 'E:\Projects\Visual Studio 2012\FsCheckLearning001\FsCheckLearning001\./../packages' to library include path

#r "FsCheck.0.9.1.0/lib/net40-Client/FsCheck.dll"  
--> Referenced 'E:\Projects\Visual Studio 2012\FsCheckLearning001\FsCheckLearning001\./../packages\FsCheck.0.9.1.0/lib/net40-Client/FsCheck.dll'  

Next I need to tell F# which module(s) to use within the dll. I looked up the name of the module using VS Object Browser

open FsCheck;; 

The property to be tested from the example.

let revRevIsOrig (xs:list<int>) = List.rev(List.rev xs) = xs;;  
val revRevIsOrig : xs:int list -> bool

And now we run the check.

Check.Quick revRevIsOrig;;  
Ok, passed 100 tests.  
val it : unit = ()  

And now creating couter-examples(s).

let revIsOrig (xs:list<int>) = List.rev xs = xs;;  
val revIsOrig : xs:int list -> bool
Check.Quick revIsOrig;;
Falsifiable, after 1 test (3 shrinks) (StdGen (768667570,295735077)):
[1; 0]
val it : unit = ()

Note that test are generated randomly so the results may vary.

Check.Quick revIsOrig;;
Falsifiable, after 2 tests (3 shrinks) (StdGen (1496431242,295735077)):
[1; 0]
val it : unit = ()
Check.Quick revIsOrig;;
Falsifiable, after 5 tests (7 shrinks) (StdGen (1734097257,295735077)):
[1; 0]
val it : unit = ()
Check.Quick revIsOrig;;
Falsifiable, after 3 tests (3 shrinks) (StdGen (1797271085,295735077)):
[1; 0]
val it : unit = ()

To see the test we can use Verbose. Note that even though it generates 100 test, the test are not unique. E.g. [] is used as test 0, 32, 65, 68. [0] is used as test 3, 11, 55. [2] is used as test 5, 46.

Check.Verbose revRevIsOrig;; 
0:
[]
1:
[-1; 1]
2:
[1; 0]
3:
[0]
4:
[1; -2]
5:
[2]
6:
[4; 5; -3; 4]
7:
[7; 4; 3; -3; 7; 7]
8:
[-5; 1]
9:
[-1; -6; -2; 5; 2; -3]
10:
[4; 3; -1]
11:
[0]
12:
[1; -5; -4; -6; 6; 0]
...
98:
[-12; -19; 2; -18; 7; -33; 36; 15; -7; -39; 20; 10; -12; 37; 15; 4; -17; 32; 10; -1;  
 -22; 27; 5; -27; -27; 22; 0; -32; 38; 17; -5; -37; 33; 12; -10]
99:
[-23; -22; 31; -27; 40; 34; -18; 1; 3; 32; -22; -35; -6; 18; -36; 36; -20; 4; 35;  
 -21; -34; -10; 21; -35; 37; -17; 7; 36; -18; -31; -7; 22]  
Ok, passed 100 tests.
val it : unit = ()

To make it easier to run the FsCheck checks, we use assertProp to run the checks within NuUnit.

If we look at this test in lib.fs

[<Test>]
let ``map is equivalent to List.map``() =
    assertProp "map" <| fun xs ->
        map (fun x -> 2 * x) xs = List.map (fun x -> 2 * x) xs

The name of the test for NUnit is map is equivalent to List.map
The name of test for FsCheck is map
The propertry for FsCheck is
map (fun x -> 2 * x) xs =
List.map (fun x -> 2 * x) xs

which is checking that the map function as defined for HOL Light lib module is the same as the F# List module function map. It does this by generating 100 random test cases, passing each test case to the Boolean conditional and reporting the results back through NUnit.

So instead of trying to hand create many test cases and encode them as test for NUnit, we let FsCheck to the work.

===

Before we can change out HOL Light functions with F# built-in functions we need to verify that they work the same. The test to ensure the same functionality are in and use FsCheck to do this.

Here is an fsx script to specifically demonstrate a failure case:

printfn __SOURCE_DIRECTORY__;;

// __SOURCE_DIRECTORY__ = <parent directories>\NHol

#I "./packages"
#r "FSharp.Compatibility.OCaml.0.1.10/lib/net40/FSharp.Compatibility.OCaml.dll"
#r "FSharp.Compatibility.OCaml.Format.0.1.10/lib/net40/FSharp.Compatibility.OCaml.Format.dll"
#r "FSharp.Compatibility.OCaml.System.0.1.10/lib/net40/FSharp.Compatibility.OCaml.System.dll"

#I "./NHol" 
#load "lib.fs" 

#r "FsCheck.0.9.1.0/lib/net40-Client/FsCheck.dll"
open FsCheck;;

// Disable ML compatibility warnings
#nowarn "62"

let test001 xs =  
    NHol.lib.rev_itlist (fun x acc -> x - acc) xs 0 = 
          List.foldBack (fun x acc -> x - acc) xs 0;;

Check.Quick test001;;

let test002 = NHol.lib.rev_itlist (fun x acc -> x - acc) [0; 1] 0;;
let test003 =       List.foldBack (fun x acc -> x - acc) [0; 1] 0;;

Code explained.

The F# Interactive (FSI) directives work off a current working directory which is called source directory. The same idea with DOS prompt and Unix systems. To identify what FSI sees as the source directory

printfn __SOURCE_DIRECTORY__;;  

Which for my system fsharp __SOURCE_DIRECTORY__ = <parent directories>\NHol

To run rev_itlist we have to inform FSI how to find them in lib module and give FSI references to the dlls needed by the lib module. Before we can bring in the lib module, the dlls must be referenced and they are in the packages directory. So we inform FSI about the packages directory.

#I "./packages"  

next reference the dlls.

#r "FSharp.Compatibility.OCaml.0.1.10/lib/net40/FSharp.Compatibility.OCaml.dll"
#r "FSharp.Compatibility.OCaml.Format.0.1.10/lib/net40/FSharp.Compatibility.OCaml.Format.dll"
#r "FSharp.Compatibility.OCaml.System.0.1.10/lib/net40/FSharp.Compatibility.OCaml.System.dll" 

Then inform FSI about the code directory

#I "./NHol"

to be able to bring in lib.fs.

#load "lib.fs" 

To run FsCheck we need to reference it's dll in the packages directory using

#r "FsCheck.0.9.1.0/lib/net40-Client/FsCheck.dll"

and open it.

open FsCheck;;

Since I don't like to see unnecessary warnings, I just disable them.

// Disable ML compatibility warnings
#nowarn "62"

The condition to check is written as a bool statement, i.e. x = y.

let test001 xs =  
    NHol.lib.rev_itlist (fun x acc -> x - acc) xs 0 = 
          List.foldBack (fun x acc -> x - acc) 0 xs;;

and run using FsCheck's Quick function.

Check.Quick test001;;

returns

Falsifiable, after 1 test (2 shrinks) (StdGen (1069121041,295736269)):
[1; 0]
val it : unit = ()

Since check reveals a case where the two checked functions are different we run both functions with the case that will cause different results.

let test002 = NHol.lib.rev_itlist (fun x acc -> x - acc) [1; 0] 0;;
let test003 = List.foldBack (fun x acc -> x - acc) [1; 0] 0;;

For test002 we get

val test002 : int = -1

and test003 we get

val test003 : int = 1

which is clearly not the same for both functions.