2010/03/31

TDD ⇒ PDD

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


main()
{
  int x, y;

  assert(x >= y);
}

と言うことだ。これは関数仕様になる。Qは無しつまりQ = { T }、R = { x >= y }である。このソースコードをプログラム検証ツールのCBMCに掛けると当然


Violated property:
  file proof0.c line 8 function main
  assertion x >= y
  FALSE

VERIFICATION FAILED

となり正しくないことが証明される。次にもともとxの方が大きい場合をQに設定して検証する。つまり以下のプログラムを検証する。ここで、__CPROVER_assume( );はCBMCで前提条件を設定するディレクティブである。

main()
{
  int x, y, tmp;
  __CPROVER_assume( x>=y ); // Q1

  assert(x >= y);
}

これは成功する。従って x >= y の時は何もしなくて良いことが証明された。次にこのQが否定された場合を考える。¬(x >= y) だから(x < y)だ。

main()
{
  int x, y;
  // __CPROVER_assume( x>=y ); // Q1
  __CPROVER_assume( x < y ); // Q2 = ¬Q1

  if (x < y) {

  }
  assert(x >= y);
}


これは失敗するのでif文の中を書いて


main()
{
  int x, y, tmp;

  if (x < y) {
    tmp = x;
    x = y;
    y = tmp;
  }
  assert(x >= y);
}

とすると

>cbmc proof0.c
file proof0.c: Parsing
proof0.c
Converting
Type-checking proof0
Generating GOTO Program
Function Pointer Removal
Starting Bounded Model Checking
size of program expression: 18 assignments
simple slicing removed 1 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Solving with MiniSAT2 without simplifier
761 variables, 2109 clauses
SAT checker: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 0.034s
VERIFICATION SUCCESSFUL

となって正しいことが証明された。(x >= y)∨(x < y)は恒真なのでQ= {T }となり仕様が満たされた。
ダイクストラの時代にはプログラム検証器が無かったので手で証明しなければならず実用にはならなかったが、今は検証器がある。現在この手法の体系化を進めている。プログラミングが終わった時に、使い古しのテストケースとバグがあるかも知れないコードを得るTDDよりはPDDの方が良いことは言うまでもない。しかもdivision by zeroの様な普通のテストではできない検証も可能である。

3 件のコメント:

  1. TDDの理解が間違っています。
    TDDはテストのパスではなく、リファクタリングの終了でもって1サイクル終了とします。

    またTDDのテストをパスしたからといって、コードの品質保証がなされるわけではありません。特にケントベックらが解説するスタンダードなTDDでは、TDDのテストを通ったからプログラムは完全だ、なんて主張はありえません。そんなこと行っている人間はペテン師か勉強不足の初心者です。
    TDDを実践せずにうわべで語る初心者がよくそこらへん誤解されていますが、貴方もその一人のようですね

    返信削除
  2. TDDはコーディング作業や設計作業そのもので、プログラムが完全かどうかの品質保証としてのメリットを一切放棄しても十分効果のでるものです。
    トンチンカンなTDD批判で恥を上塗りするのはやめて、もう少し謙虚に技法や技術を勉強されてはどうですか?

    返信削除
  3. ご指摘ありがとうございます。修正しておきます。

    返信削除