欲しいのはバグはあるかも知れないが取りあえず動作する綺麗なコードではなく、まずバグのないコードだ。
この点を改善するにはどうするか。実は良いアイディアが浮かんだ。自動テストツールではなく、プログラム検証ツールを使用して正しいことを証明しながらプログラミングをおこなう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の様な普通のテストではできない検証も可能である。
投稿
