Wednesday, July 4, 2012

Specification-based testing (FsCheck)

This is how I like to write specification tests. Notice the lack of ceremony.
[<Property(Arbitrary=[| typeof<ArbitraryModifiers> |])>]  
let ``Closed under multiplication`` (y : WholeNumber) (z : WholeNumber) =
         (WholeNumber.get y) * (WholeNumber.get z) >= 0

Test.Geometry.Closed under multiplication [FAIL]
Falsifiable, after 3 tests (0 shrinks) (StdGen (603380185,295587877)):
(WholeNumber 13118, WholeNumber 227510903) 

In other words, the system is able to automatically prove that whole numbers (implemented on top of .NET Int32) are not, in fact, closed under multiplication because of integer overflow, since 13118 * 227510903 = -514245166.

Then, I change WholeNumber so that it is built on top of bigint (arbitrary-sized integers as in math, not computer architecture) and alter the test slightly to use 0I (bigint version of zero).
[<Property(Arbitrary=[| typeof<ArbitraryModifiers> |])>]  
let ``Closed under multiplication`` (y : WholeNumber) (z : WholeNumber) =
         (WholeNumber.get y) * (WholeNumber.get z) >= 0I

Tests complete: 1 of 3
Tests complete: 2 of 3
Tests complete: 3 of 3
3 total, 0 failed, 0 skipped, took 1.790 seconds

Voila! My program now matches my spec.

FsCheck + Xunit = WIN


Hahahahaaaa!!! That is ME laughing at YOU, cruel world.
    -Jordan Rixon

I could not love thee, dear, so much,
Loved I not Honour more.

No comments: