implyとequivalent及びBranch coverageとDecision coverage

Twitterで話していたがまとめて話さないと伝わらないので、まとめてみる

ここに、Branch/Decision Testingという記事があって、冒頭に

For components with one entry point 100% Branch Coverage is equivalent to 100% Decision Coverage (入り口が一つのコンポーネントに対しては100%BCは100%DCと等しい)

と書いてある。

equivalentとは?
等しいのだからBDが100%ならDCも100%になりその逆も成立する。等価性には対称律が成立する。

入り口が複数あるとは?
構造化プログラム言語を使っていると関数の入り口は一つに決まっているが、昔のFortranのentry文を使うとサブルーチンの入り口を複数作ることができる。今でもOSのディスパッチャ等はマルチエントリの関数として実装されている。

この様な、プログラムでは100% Branch Coverage is equivalent to 100% Decision Coverageでは無くなる。

これとは別に


「デシジョンカバレッジとブランチカバレッジはお互いに、"A implies B"と定義されています。なので"A=B"となりますが、・・・」

と言うつぶやきがあり、これは違うでしょうと言ったのだけれど上の話と混ざってしまって140字では伝わらない。



implyとは?
implyとequivalentは違う。implyは片方向で、equivalentは両方向である。A implies B and B implies Aの時にequivalentと言って良い。これが対称律だ。

つまり

100%DC = 100%BC
DC⇒BC

は成立するが、

DC=BC

は成立しない。ここでBCと表しているのは、Branch/Decision Testingという記事で言えば

BC = {
B1 -> B2
B2 -> B3
B2 -> B9
B3 -> B4
B3 -> B5
B4 -> B8
B5 -> B6
B5 -> B7
B6 -> B8
B8 -> B2
}


と言う制御ブロック間の実行順序対の集合である。これは、元のプログラムのフローグラフの辺の集合として得ることができる。

一方、DCの方はプログラム内の論理判断の結果なので

DC = {

B2 -> B3

B2 -> B9

B3 -> B4

B3 -> B5

B5 -> B6

B5 -> B7

}

となる。従って

DC⇒BC

が成立していることが分かる。これは、DCの任意の要素を持ってくるとそれはBCの要素にもなっていると言う意味である。DCの要素ならばBCの要素でもある。これを省略して「DCならばBCである」と言うこともある。また

BC⇒DC

が成立していないことも分かる。これで、話は終わりかも知れないが、それなら100%DCだけど100%BCにならない例を見せてみろと尤もな突っ込みがあった。これは既に、シングルエントリの場合には、反例はないと言っているので、マルチエントリの場合を考えれば良いので、先のフローグラフの途中から実行を開始するようなパスを追加すれば良い。

だいたい
implyを暗黙に・・・等という訳の分からない日本語にするのが良くない。ことばを置き換えただけで分かったつもりになってしまう。

「ならば」と等価の区別はきっちり付けないといけない。アリバイがないから犯人にされてしまう世の中にはなって欲しくない。

カバレッジは幾つもあるが、そのカバレッジが定義する全体集合を実際に手で作って見れば色々なものが見えてくる。面倒くさいが実際に集合を作ってみて包含関係を見れば一目瞭然である。

Wot, no chickens?

Javaにはリアルタイム性が無いと言うと、ガベージコレクタの話題かと思うが、それだけではない。以下の二つも問題である。

1. Javaには待ち行列が二つある。Synchronizedによる待ち行列とwait/notifyによる待ち行列である。この二つの待ち行列のせいでライブロックが発生する。これはJava仕様の問題だろう。
2. それからもう一つ、待ち行列がFIFOではなくLIFOになっていることである。どこまでがJava仕様でどこからがVM実装依存なのか分からないが、現在ダウンロードできるJavaの実行環境はLIFOになっている。LIFOだと後から来たスレッドが先に処理されるので、オーバーロード時には最初に来たスレッドは永遠に待たされる。優先度付き待ち行列のポリシーはVM実装時に変更できないとどこかで読んだ気がするが、この記憶が正しければJava仕様の問題だろう。

これだけJavaが使われていて誰も問題にしないのは謎である。しかし、Androidがカーナビなどでも利用されるようになってくると問題になるのだろうと思う。

この問題を最初に指摘したのはKent大学のPete Welchで「wot, no chickens?」で検索すると今でも関連するページを見ることができる。サンプルコードも掲載されているので実験することができる。インタフェース誌にも小山尾 登氏の解説記事[1][2]が掲載されている。小山尾氏の実験によって現状のJavaVMの待ち行列がLIFOであることが分かった。IBMのサイト[3]でも説明されている。
Javaの問題点を指摘するためにBristol大学のAlan ChalmersがIEEE宛に1997年にレターを以下のメンバーと連名で送ったが無視されたらしい。レターの本文はしばらくWeb上にあったが今はアクセスできなくなっている。

Alastair Allen (University of Aberdeen, UK)
Andre Bakkers (University of Twente, Netherlands)
Richard Beton (Roke Manor Research Limited, UK)
Alan Burke (Aurigor Telecom Systems, Canada)
Alan Chalmers (University of Bristol, UK)
Barry Cook (University of Keele, UK)
Michael Goldsmith (Formal Systems (Europe) Ltd, UK)
Gerald Hilderink (University of Twente, Netherlands)
Ruth Ivimey-Cook (Advanced RISC Machines Ltd, UK)
Adrian Lawrence (University of Oxford, UK)
Jeremy Martin (University of Oxford, UK)
Nan Schaller (Rochester Institute of Technology, USA)
Dyke Stiles (Utah State University, USA)
Oyvind Teig (Autronica, Norway)
Paul Walker (4 Links, UK)
Peter Welch (University of Kent, UK)

それで、この問題を放置するわけにも行かないのでWelch達はCSPを使ってJavaの通信用ライブラリJCSP[4]を作成して公開している。使い方は、中原氏のホームページ[5]に解説がある。今後、組込でJavaを使うのであればJCSPを使った方が良いのではないかと思う。


[1] 並列プロセッサXMOSの検証環境PAT2
[2] UPPAALによる時間仕様検証
[3] JavaプログラマーのためのCSP　第1回
[4] Communicating Sequential Processes for JavaTM (JCSP)
[5] CSPモデルプログラミング

回文数式作成プログラム

プログラム検証ツールを使って回文数式を作る。
例えば

42+46=64+24


// 回文数式作成
void main()
{
  int a1, a2, b1, b2, A1, A2, B1, B2;
  __CPROVER_assume(a1 > 0 && a1 <10 && a2 > 0 && a2 < 10 && b1 > 0 && b1 < 10 && b2 > 0 && b2 < 10);
  A1 = 10*a1 + a2;
  A2 = 10*a2 + a1;
  B1 = 10*b1 + b2;
  B2 = 10*b2 + b1;

  assert((A1+B1) != (A2+B2));
}

このプログラムをCBMCに掛ければ検証に失敗して

State 7 file anagram.c line 9 function main thread 0

----------------------------------------------------

  anagram::main::1::A1=42 (00000000000000000000000000101010)

State 8 file anagram.c line 10 function main thread 0

----------------------------------------------------

  anagram::main::1::A2=24 (00000000000000000000000000011000)

State 9 file anagram.c line 11 function main thread 0

----------------------------------------------------

  anagram::main::1::B1=46 (00000000000000000000000000101110)

State 10 file anagram.c line 12 function main thread 0

----------------------------------------------------

  anagram::main::1::B2=64 (00000000000000000000000001000000)

State 11 file anagram.c line 14 function main thread 0

----------------------------------------------------

  c::main::$tmp::tmp$1=FALSE

Violated property:

  file anagram.c line 14 function main

  assertion (A1+B1) != (A2+B2)

  FALSE

VERIFICATION FAILED

を得ることができる。

7/1 追加
魔方陣の解き方
CBMCで魔方陣を作成するプログラムが公開されています。

単体テストできない関数

ヨーロッパの鉄道の安全規格[1]で一番厳しいSIL4ではブランチテストの100%カバレッジが求められるらしい。if文がネストしている複雑な関数の場合、そこにたどり着く入力データを作り出すのはなかなか難しい。CBMCを使って簡単にテストデータを生成する方法としてassert(0)を埋め込む方法がある。到達したい場所にassert(0)を仕込んで置いてCBMCで検証をすればCBMCが向きになってそこまで行って転けてくれるのでたどり着く方法が明確になる。必要があればprintf文も仕込んでおく、さらにテキストファイルに書き出すようにすれば、テストツールに掛けられる形でテストケースを得ることができる。

しかし、この方法も構造化されたプログラムでないとうまく行かない。構造化されたプログラムというのは、逐次、分岐、繰り返し構造だけでできているプログラムで、前方に跳ぶgoto文とか入れ子にならない繰り返しを持っていないプログラムである。今時、この様なプログラムはアセンブラで書かれたOSのディスパッチャぐらいだろう。ところが、並列性がある場合は任意のgoto文が動的に入るのと同じだからうまく行かない。要するに単体テストできないのと同じである。
グローバル変数を使っていても並列性が無ければ単体テストはできるが、それがvolatileなものだとそうはいかない。いちいちvolatile宣言しないとテスト以前にコンパイルがチャンとできているか心配になる。

並列性がある場合には、節操なくグローバル数を使うことは控えなければならない。空海がどのように並列に文章を書くのか、文章だけはできていて出力だけが並列なのか、文章も考えながらつじつまの合うものを書き出すのか、これはアーキテクチャがぶれていては実現できない。
グローバル変数を多用して、並列性のあるシステムを作っていて、単体テストもチャンとやってますとか言う組織は多いけれどどんな単体テストをやっているのだろうか。

[1] European Committee forElectrotechnical Standardization. Railway Applications -
Communication, signalling and processing systems - Software forrailway control
and protection systems, http://www.cenelec.eu

PDD その2

インタフェース誌にPDDのアイディアを書いた[1]。基本的な手順は、

1.      プログラムの目的を事後条件として表す。assert文で表現する。

2.      入力条件を場合分けし、それを事前条件とする。assume文で表現する。

3.      assume文の範囲でコーディングをおこない、検証をパスさせる。

4.      パスさせる過程で反例を分析して、分析結果はコーディングまたは事前条件に反映させる。

5.      残りの入力条件について同様に検証をパスさせる。

6.      全ての入力条件に対して検証が終わったら、事前条件を整理する。

基本的にはプログラムSを下のような形にして、Q∧Ｓ⇒Rを満たす様にする。QとRがプログラムの仕様である。入力条件は実装後はテスト条件として使用できる。

assume(Q);
S;
assert(R);

似たような形をコンピュータのセキュリティ改善に使っている論文があった[2]。この論文ではダイクストラの最弱事前条件を使っている。プログラム検証ツールを使用すれば自動化できる部分もありそうだ。

何もしないスキッププログラムの場合は、S=TrueなのでQ⇒Rになる。プログラム検証ツールは含意論理式の証明器としても使えることが分かったので、[1]ではちょっとした実験を紹介した。この実験を発展させて仕様書検証に使えないか検討してみた。すなわち、VDMで言うところの、陰関数定義をCで書いて検証できれば、仕様検証になる。やってみたら、確かにできそうだが、C言語で事前条件・事後条件を書くのが結構大変である。おかげで、述語論理を使えるVDMや時相論理を使えるモデル検査ツールの便利さが分かった。
モデル検査ツールはテストケースを用意しなくても検証できるが、述語論理式はテストケースが必要になる。と言うことはPDDの過程で作成するテスト条件が述語論理式をC言語で記述するヒントになるのかも知れない。
自然言語から直接Cの様なプログラム言語を書き出すのと、一端、述語論理式を経由するのでは、後者の方が絶対に楽なはずだ。壁の正体は何だろうか?

[1]新・組み込みソフトへの数理的アプローチ（第12回）
テストとプログラム検証――TDD（テスト駆動開発）におけるテスト

[2]B. V. Chess. Improving Computer Security using Extended Static Checking. In Proc of. 2002 IEEE Symposium on Security and Privacy, pages 160-173, 2002.

レビューの信頼性

レビューする時、間違っているのに正しいとしてしまう間違いと、正しいのに間違っているとしてしまう間違いの二通りの間違いがある。前者をtype-1、後者をtype-2の間違いとする。またそれぞれの発生確率をe1、e2とする。要するにtype-1は見落とし、type-2は濡れ衣を着せてしまうことに対応する。

一人で2回レビューする時、1回目で間違いとしたものは見直さない場合には、見落としの確率は低くなるが、濡れ衣の確率は高くなる。xをe1またはe2としてプロットすると上図のようになる。つまり、見落としの方は二回連続で見落とさない限り検出されるので、見落とし確率はe1*e1になる。0 < e1 < 1なので小さくなりレビューの信頼性は向上する。濡れ衣は一度着せられてしまうと脱げないので、着せられてしまう確率は高くなるのである。濡れ衣を着せられない確率は1-e2で二回連続で着せられない確率は(1-e2)*(1-e2)になる。従って、一度でも着せられてしまう確率は1-(1-e2)*(1-e2)になる。これが上図の濡れ衣確率である。レビューしている本人にはどっちの間違いを犯したか判断は付かないというか、そもそも気づかないから間違いなのでどうしようもない。

逆に、一回目のことはすっかり忘れたことにして二回目のレビューをして両方で検出されたもののみを間違いとする場合は、今度は見落とし確率が高くなる。二人で1回レビューする場合で、二人が一致したもののも間違いとする場合も同様である。どちらかが間違いとしたものを間違いとする場合には、再び濡れ衣確率が高くなる。要するに必ずどちらかの間違い確率が高くなってしまう。

そこで、二人で二回レビューすることにすると、間違いのタイプによって挙動が変わる。見落とし型の間違いは以下のようになる。一回の間違い確率が0.38より大きいと信頼性が下がる。

濡れ衣型の間違いは以下のようになり、一回の間違い確率が0.61以上だと信頼性が下がる。

いずれにしても、おっちょこちょいな人が混じっているとレビューの信頼性は悪化する。と言うかやらない方が良いかも。

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の様な普通のテストではできない検証も可能である。