Back when I was taking my Computer Science degree at University I learned all about ‘Formal Methods’ (when I wasn’t playing pool, badly, that is). The main reason to use Formal Methods is to prove the correctness of programs. By stating a logical pre-condition for a block of code you can apply a sequence of logical steps to it that each correspond to the behaviour of each of the statements in the block. If when you reach the end of your block your transformed pre-condition is the same as the logical post-condition then your block is proven correct. If you do this for your entire program then it as a whole is proven correct.
So why doesn’t anyone really do this outside of academia? Basically because:
– Coming up with pre- and post- conditions that represent exactly what you want your program to do is hard
– The actual process is equally hard
– .. meaning that the whole thing is slow
OK, now flip to what I do now. I’m a big fan of ‘Extreme Programming’ techniques including Test Driven Development (TDD) which is an evolution of unit testing. Why do we do unit testing? Partly to try and ‘prove’ that each part of our program works. Its not really absolute proof since we never know if our unit tests uncover all possible bugs in the code, but its a good approximation. In fact as we add more unit tests it becomes an even better approximation of proof.
Anyway, why am I rambling about this? Well, the academic in me (which isn’t allowed out very often) always had a bit of a bad feeling about unit testing due to its lack of proof. But recently I was talking to a couple of ThoughtWorkers about analytical and numerical processes in Maths. With analysis (or calculus) you prove the answer to a problem using Mathematical logic. Some problems though are either (1) too hard to solve like this or (2) take too long to solve so you can also use numerical methods. These never give you the exact solution but through a succession of repeated calculations you can tend to (or hone in on) the solution until you have an answer that is ‘good enough’.
To me, this relationship of analysis and numerical methods seems strikingly similar to that of formal methods and unit testing. Since numerical solutions are academically valid this makes the academic in me happier about unit testing.
TDD isn’t just about testing though – its also a method of actually deciding how to write a program. You start with a failing test, write some code that fixes this test in the simplest way possible, refactor your program to remove duplication, and then repeat. In my Formal Methods studies at University I also saw how you could actually write a program based on a logical specification and a set of rules related to the ‘correctness proving’ rules. (See here). So both TDD and Formal Methods offer a way of ‘generating’ code based on testable specification (programmatic assertions for TDD, logical specifications for Formal Methods.)
In conclusion, this argument itself doesn’t prove anything (!) but in my own mind at least showing a relationship between Formal Methods and TDD strengthens the case for TDD being a valid, and valuable, technique for writing software.
Mike Roberts