I am speaker at ALE 2014 in Krakow
Posted: August 06, 2014
My presentation "Let Tests Drive or let Dijkstra Derive?" has been accepted at the unconference ALE 2014 in Krakow.
Here is the abstract of the presentation:
Test-Driven Development is presented as the one and only way to write code. Some people consider you not a professional software developer if you do not use it. Uncle Bob uses TDD to solve the Primes Kata with just three lines of code. These three lines were justified by only seven tests. However, tests have one big problem: tests can only prove the presence of bugs, not their absence. So how does TDD help you writing correct programs?
Prof. E.W. Dijkstra, winner of the Turing Award, developed a formal way of deriving and proving algorithms. Formal proofs are constructed with pre- or postconditions. Rules to prove the postcondition of a single assignment and a single if-statement are shown. Using an invariant and a bound function the postcondition of a while-loop can be proved. Using these simple rules a solution of the Primes Kata is derived.
The formal proof of the correctness for these three lines make one thing clear: seven tests are not sufficient to prove this algorithm!
Do not fear very detailed and formal mathematical proofs. The derivations are presented in a practical and informal way.