As programmers we often want to express that a special property holds for a method, e.g. we want to say that the associativity law holds for list concatenation. In F# we could define a concat method like this:

As programmers we could write a couple of unit tests which try to check the associativity law. With NUnit enabled we could write this:

But the question is: did we cover all interesting cases? In computer science we have a method to prove that the property holds for all lists. This methods is called structural induction (see also this video lecture by Martin Odersky) and would look like this:

##### 1) Rewrite the code as equations

concat ([],ys) = ys [CON1] concat (x::xs,ys) = x :: concat(xs,ys) [CON2]

##### 2) Rewrite the property as an equation

concat(concat(xs,ys),zs) = concat(xs,concat(ys,zs))

##### 3) Check the base case

concat(concat([],ys),zs)

= concat ([],zs) // using CON1 = [] // using CON1

concat([],concat(ys,zs))

= concat (ys,zs) // using CON1

= [] // using CON1

##### 3) Show the inductive step

concat(concat(x::xs,ys),zs)

= concat (x::concat(xs,ys),zs)) // using CON2

= x :: concat(concat(xs,ys),zs) // using CON2

= x :: concat(xs,concat(ys,zs)) // induction hypothesis

= concat(x::xs,concat(ys,zs)) // using CON2

This math is very clean and shows that the associativity law holds for all lists. Unfortunately even with a slightly more complicated sample this gets at least tricky. Try to prove that *reverse(reverse(xs)) = xs* with **reversed** defined as:

As you will see the naÃƒÂ¯ve approach with structural induction will fail (for a nice solution see this video lecture).

There is even a bigger problem with the proof: one assumption of induction is referential transparency of the given functions. We canÃ¢â‚¬â„¢t always assume this.

So we canÃ¢â‚¬â„¢t always (easily) proof code properties and we donÃ¢â‚¬â„¢t want to write too many unit tests – then what can we do?

One compromise solution is to use a tool which systematically generates instances for our tests. There are a couple of tools out there, e.g. there is QuickCheck for Haskell or PEX for .NET. In F# we can use a tool called FsCheck:

Of course a test like this doesnÃ¢â‚¬â„¢t prove that the property holds for all lists, but at least it verifies all bases cases and probably a lot more cases than one would manually do.

If you introduce a bug you get a nice report, which even shows a counterexample:

It’s even possible to add these tests to your test suite and to run them during the CI build. So don’t stop at classical unit test – check code properties!

Tags: F#
[…] Steffen Forkmann presented “Testing, proving, checking Ã¢â‚¬â€œ How to verify code properties“. […]

Pingback by F# Weekly #50, 2012 « Sergey Tihon's Blog — Sunday, 16. December 2012 um 21:07 Uhr