TDD ⇒ PDDダイクストラは、テストでバグの存在は示せるがバグのないことは示せないと言っていた。一方で、TDDはテストを重ねながらプログラミングをおこない、用意したテストが全部通ったらプログラム完成と言うアプローチだ。と誤解しやすいが実は単なる開発プロセスに対する提案である(10/2)。 欲しいのはバグはあるかも知れないが取りあえず動作する綺麗なコードではなく、まずバグのないコードだ。 この点を改善するにはどうするか。実は良いアイディアが浮かんだ。自動テストツールではなく、プログラム検証ツールを使用して正しいことを証明しながらプログラミングをおこなうPDD(Proof driven development)だ。 プログラムSの証明とは、Qを事前条件、Rを事後条件として、{Q} S {P}が恒真であることを示すことだ。たとえば、二つの整数x, yを与えられてxが大きい値になるように、値を入れ替えるプログラ
