# 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