Rash thoughts about .NET, C#, F# and Dynamics NAV.


"Every solution will only lead to new problems."

Tuesday, 11. December 2012


Testing, proving, checking – How to verify code properties

Filed under: F#,Informatik — Steffen Forkmann at 13:12 Uhr

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:

fscheck

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:

1 Comment »

  1. […] 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

RSS feed for comments on this post. | TrackBack URI

Leave a comment

XHTML ( You can use these tags): <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong> .