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

## 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: 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