Property-Based Testing with FsCheck

class: center, middle

# Property-Based Testing

## using FsCheck

by [gimpf](http://gimpf.org) for [r³](http://realraum.at)

.smallBottomLeft[[under CC-BY](http://creativecommons.org/licenses/by/3.0/), (created with [remark](https://github.com/gnab/remark))]

---
# What is Property-Based Testing?

_a.k.a. specification-based testing, hypothesis testing_

* A way to assist automated software testing.
* Developers define a set of logical properties that must hold true.
  * Logical property: a function with a boolean result.
* Test framework tries to falsify these assertions.

---
# Motivation: All is well!

.smaller[

Pattern: "^(a*,)+$"
        ms    text
         0    "a,a,"
         0    "a,a,a,"
         0    "a,a,a,a,a,"
         0    "a,a,a,a,a,a,a,a,a,"
         1    "a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,"
         1    "a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,"
         0    "a,aa"
         0    "a,a,aa"
         0    "a,a,a,a,aa"
         1    "a,a,a,a,a,a,a,a,aa"
         1    "a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,aa"
         2    "a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,aa"
        
]

--
Linear growth.  You don't see it here, because...

---
# Motivation: All is not well.

.smaller[

Pattern: "^(.*?,)+$"
        ms    text
         0    "a,a,"
         0    "a,a,a,"
         0    "a,a,a,a,a,"
         0    "a,a,a,a,a,a,a,a,a,"
         1    "a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,"
         1    "a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,"
         0    "a,aa"
         0    "a,a,aa"
         1    "a,a,a,a,aa"
        21    "a,a,a,a,a,a,a,a,aa"
      5273    "a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,aa"
    ......    "a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,a,aa"

]

--
The last one got interrupted after more than an hour.

Exponential. Because during some refactoring we made it "more flexible".

---
# Motivation

We want to avoid such patterns even when using match-timeouts,
and review will never be perfect.

Testing such stuff is done via "fuzzing", one of the many things
you can do with a good property-based testing framework.

---
# Why use it?

* Reduce time to write coarse tests.

It is faster to specify one invariant than to write out test-cases.

* Reduce time to find the minimal failing example.

Data reduction can be automated.

---
# Why use it?  
 
* Improve test coverage.

Most frameworks report statement coverage.  Good branch/state
  coverage is much more difficult to achieve!
  
  Fuzzing helps finding edge-cases, stability issues.

---
# Where use it?

* Works well for unit-tests.
* Works well for integration tests.
* Works well for system tests.
* Acceptable for heating.

---
# Existing Libraries

* Haskell [QuickCheck][] released 1999
* Everyone ported it to everywhere  
  (to varying degrees):
  * [PropEr][] for Erlang (among others!)
  * JVM/Scala [ScalaCheck][]
  * [FsCheck][] for .NET (F#, C#)
  * Python [hypothesis][]
* most (semi-)functional PLs have acceptable ports

**Most of the time, usage is very similar!**

[QuickCheck]: http://www.cse.chalmers.se/~rjmh/QuickCheck/
[PropEr]: http://proper.softlab.ntua.gr/
[ScalaCheck]: https://github.com/rickynils/scalacheck
[FsCheck]: http://fscheck.codeplex.com/
[hypothesis]: https://pypi.python.org/pypi/hypothesis

---
# PBT Concepts and Keywords

* **Arbitrary**  
  a placeholder for a value
* **Generators**  
  generate arbitrary values
* **Size**  
  a vague measure of complexity
* **Shrinkers**  
  simplify a falsified test-case
* **Universally quantified properties**  
  ∀x: P(x)
* **Conditional properties**  
  ∀x: C(x) ⇒ P(x)

---
# FsCheck Features in Keywords

* **Generator Combinators**  
  use existing generators to build new ones
* **Generator Expressions**  
  EDSL for writing generators
* **Stateful Testing**  
  model the state of a black-box and check behavior/side-effect of events
* **Lazy Properties**  
  F# is not Haskell, so this comes in handy
  
---
# FsCheck Features in Keywords

* Expected Exceptions
* Timed Properties
* Trivial and Classified Test-Cases
* Collecting test-data
* Property Combinators
* Property Labels

---
# FsCheck: Our base case

open FsCheck
    
    type Properties () =
        static member ``addition is commutative`` a b =
            a + b = b + a
    
    module Program =
        [<EntryPoint>]
        let main args =
            Check.QuickAll<Properties> ()
            0

--
.output[

--- Checking Properties ---
    Properties.addition is commutative-Ok,
    passed 100 tests.

]

---
# Think about your properties!

What is the result of this?

static member ``addition is commutative``
            (a : float) b =
        a + b = b + a

--
.output[

--- Checking Properties ---
    Properties.addition is commutative-Falsifiable,
    after 55 tests (2 shrinks)
    (StdGen (1855018204,295717156)):
    (nan, 27.0)

]

---
# Related: Contracts

All those make good properties:

* Preconditions
* Postconditions
* Invariants

These can also be achieved through contracts
(in some languages).

Property based testing extends this to stuff not declarable at compile-time.

---
# Combine Properties

let ``product is 0 iff a factor is 0`` a b =
        ((a <> 0 && b <> 0) ==> (a * b <> 0)) .&.
        ((a = 0  || b = 0)  ==> (a * b = 0))

---
# Label Properties

let ``product is 0 iff a factor is 0`` a b =
        "non-zero" @| ((a <> 0 && b <> 0) ==> (a * b <> 0)) .&.
        "zero"     @| ((a = 0  || b = 0)  ==> (1 + a * b = 0))

.output[

Falsifiable,
    after 1 test (0 shrinks) (StdGen (306885404,295717844)):
    Label of failing property: zero
    (0, 0)

]

---
# Classify Test-Cases

let ``classify tautology`` a b =
        (a = b || a <> b)  ==> (a = b || a <> b)
        |> trivial (a = 0)
        |> classify (a = b) "equal"
        |> classify (a <> b) "non-equal"
        
.output[

Ok, passed 100 tests.
    84% non-equal.
    7% non-equal, trivial.
    4% equal, trivial.
    4% equal.

]
        
---
# Lazy properties

let lazyProperty a = a <> 0 ==> lazy (1/a = 1/a)

---
# Test for Exceptions

let ``throw unconditionally`` () =
        throws<ArgumentException,_>
          (lazy (raise <| ArgumentException("")))

---
# Timed Properties

let ``regex is nice`` text =
        let regex = Regex(".*")
        lazy for i = 1 to 1000 do regex.IsMatch(text) |> ignore
        |> within 0
        
.output[

Timeout of 0 milliseconds exceeded,
    after 1 test (0 shrinks) (StdGen (627880440,295717849)):
    ""
    
]

---
# But we cannot test it all too well...

let ``is regex nice?`` text =
        let regex = Regex( "^(.*?,)+$"
                         , RegexOptions.ExplicitCapture)
        lazy for i = 1 to 10000 do
                 regex.IsMatch(text) |> ignore
        |> within 10

.output[

Ok, passed 100 tests.

]
        
Could have failed with only 18 characters (or less)...

---
# Universal Quantification Over Custom Set

let ``is regex nice now?`` () =
        let textGen =
            Arb.fromGen
            <| gen {
                let! chars =  Gen.sized (fun s ->
                    Gen.elements [ 'a' ; ',' ]
                    |> Gen.arrayOfLength (10 * s))
                return String(chars) }
        forAll textGen Properties.``is regex nice?``

.output[

Timeout of 10 milliseconds exceeded, after 3 tests
    (0 shrinks) (StdGen (566056109,295717856)):
    <null>
    ",a,,,,,a,a"

]

---
# Stateful Testing

Not everything is a pure function.  Testing MVC projects,
quasi-remote services etc. is usually state-dependent.

This is done through simplified specification,
bound together with the actual commands.

---
# Stateful Testing

[_stolen from the doc_][statedoc]

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()

[statedoc]: http://fscheck.codeplex.com/wikipage?title=Stateful%20Testing

---
# Stateful Testing

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 _ = Gen.elements [inc;dec]

---
# Stateful Testing

.output[

> Check.Quick (asProperty spec);;
    Falsifiable, after 4 tests
    (1 shrink) (StdGen (1906253113,295281725)):
    [inc; inc; inc; dec]

]

---
# Some Goodies

* FsCheck can fake function values.
* xUnit (only xUnit) integration through `[<Property>]`
* Usable from C#:

.breaker[

.cs 
    Spec.ForAny<int>(a => 1 / a == 1 / a)
        .When(a => a != 0)
        .QuickCheck("DivByZero");

]

---
# FsCheck Wishlist

* Parallelism Tests

would require byte-code transformation
  
* Simpler Integration with Mock/Fake Frameworks

currently duplicated code

---
# Links

* [QuickCheck][]
* [PropEr][]
* [ScalaCheck][]
* [FsCheck][]
* [hypothesis][]