2010/07/22

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

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

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


2010/07/18

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モデルプログラミング