研究速報
JML(Java Modeling Language) [5] は Java プログ
Java に対するループインバリアントを含む Daikon

ラムコード中にコメント形式で表明を記述するための生成アサーションの妥当性評価

形式的記述言語である．

宮本 敬三†岡野 浩三†（正員）

Daikon は生成した表明を JML 形式など様々な形式

楠本 真二†（正員）で出力できる．また，生成された表明を JML 形式でAdequacy evaluation of assertions for Java including loop invari-

対象プログラムに挿入する等，利便性の高い機能も有ants generated by Daikon
Keizo MIYAMOTO† , Nonmember, Kozo OKANO† , andShinji KUSUMOTO† , Members†している．

ESC/Java2 [4] はプログラム中に JML で記述した

大阪大学大学院情報科学研究科，560-8531 豊中市 待兼山町

表明を静的解析により判定するツールである．表明をGraduate School of Information Science and Technology, Os-

満たすか否かの情報とともに，満たさない場合は理由

aka University, Toyonaka, Osaka, 560-8531 Japan

あらまし

Daikon が生成する事前・事後条件の表を出力する．

3. 評価
3. 1 評価の目的と基準

明を ESC/Java2 で評価すると再現率，適合率ともに評価実験の目的はメソッド，ループ部に対して生成高いという研究結果がある．小規模のプログラムに対された表明の妥当性の検証である．Daikon が動的解し，事前・事後条件，ループ不変式の再現率，適合率

析により生成した表明の適合率と再現率，F 値を求めを ESC/Java2 および人手で行った．その結果を示し，ることにより生成された表明の妥当性を評価する．な考察を与える．

お，ループ不変式は著者らが開発したツールを用いて，キーワード

Java, 事前条件, 事後条件, 不変式,Daikon, JML, ESC/Java2

間接的に Daikon に生成させた．適合率 (P)，再現率(R)，F 値 (F) は，Daikon により生成された全表明数

1. ま え が き(A), ESC/Java2 において正しいと判定されたアサー

DbC [1] はクラスとクラスの利用側の間における仕ション数 (E)，人が記述した必要な表明数 (C), 人が様決定を契約とみなすことでソフトウェアの信頼性，記述した必要な表明と Daikon により生成された表明保守性を高めることを目的としている．この契約を記の共通集合の要素数 (N) を用いて以下のように定義さ述する表明の自動生成ツールの一つである Daikon は，れる．

テストケース上でプログラムを実行し動的解析を行う•

適合率 : P (P = E/A)

ことで表明を自動生成する [2]．しかし，Daikon が生•

再現率 : R (R = N/C)

成できるのはメソッドの事前条件，事後条件のみであ•×R)
F 値 : F (F = 2×P
P +Rる．だが，ループ不変式は繰り返し処理の停止性や妥

この F 値が高いほど妥当性が高いとする．

当性に関連するプログラムの可読性，保守性の向上，検また，生成された表明の再現率を評価するための基証自動化という観点から重要である [1]．一方，Daikon

準として，必要な表明，不要な表明を以下のように定の表明生成能力については文献 [3] で ESC/Java2 [4]義する．

で再現率，適合率を検証すると，ともに高い結果 (約•ドの内容を理解した人間が記述した表明90%) が得られたと報告されている．しかし，表明自動生成の実用的観点からは，ループ不変式の評価や人の観点からの評価も大事である．

必要な表明:プログラムの動作内容，ソースコー•

不要な表明：特定のテストケースに依存し一般的には成立しない表明

そこで，本研究では Java プログラムに対し，事例えば，入力された配列に対してインサーション

前・事 後 条 件 ，ル ー プ 不 変 式 を Daikon で 生 成 し ，ソートを行うメソッドに対して要素数 10 の配列 a をESC/Java2 [4] と人手で，生成表明の妥当性を評価テストケースとして Daikon で表明を出力させる．こした．その結果，人手で評価した場合，Daikon が生のときループカウンタとして用いられている変数 i に成したメソッドとループ部の表明の妥当性は現状では関する事後条件として [ensure i==10] という表明がやや低いということを確認した．

出力される．この表明は動作結果としては正しいが入2. 準力される配列の要素数は固定ではないので，一般的に備

JML, Daikon，ESC/Java2 について簡単に述べる.

は成立しない．このような表明を不要な表明とする．

電子情報通信学会論文誌 A Vol. Jxx–A No. xx pp. 1–3

xxxx 年 xx 月

1

電子情報通信学会論文誌 xxxx/xx Vol. Jxx–A No. xx
表 1 対象プログラム
Table 1 Target programs
No.
123

プログラム名 No. プログラム名
Sum.java4iSorting.java
Min.java
5
qSorting.javabSorting.java 6
calc.java

考えられる．メソッドの事前条件，事後条件はクラスのフィールド変数，メソッドの仮引数，返り値の間に成立する条件を求めることになる．一方，ループ部の事前条件，事後条件の場合はフィールド変数，メソッドの仮引数，ローカル変数の間に成立する条件を求めることになる．対象プログラムには，ローカル変数は3. 2 評価対象のあらまし複数存在しているために，ループ部の事前条件，事後評価対象として表 1 に示す 6 種類のプログラムを用

条件のほうがメソッド部より考慮すべき条件が複雑にいた．プログラム名が内容を表している．calc.java はなる．この結果，適合率が文献 [4] の値より低下した

逆ポーランド記法の数式を計算するプログラムである．と考えられる．また，再現率が低下の原因としては，これらのプログラムはループがアルゴリズム中で重要判定方法の違いが考えられる．文献 [3] では再現率をな役割をはたしている．また，条件分岐，配列変数な求める際に ESC/Java2 による判定を用いている．しどループ以外にもプログラムに重要な要素を含んでいかし，本稿では人手による判定を用いた．この結果，るという点でも評価対象に適していると考える．

再現率が文献 [3] の値より低下したと考えられる．ま3. 3 結果た，表 2 の結果をプログラム別に見ると calc.java の

表 1 の対象プログラムに対し生成された表明のう再現率，F 値が他のプログラムよりも低いことがわかち，ループ部に対して生成されたものの結果を表 2 にる．これは，他の 5 つのプログラムへのテストケース示す．また，人手で適合率を求めた場合のメソッドとは Java の乱数生成メソッドを用いて自動生成したが，ループ部の表明の比較結果を表 3 に示す．

calc.java へのテストケースは自動生成ではなく人手で4. 考察作成したために入力データ数が少なくなってしまった，

結果は略すが，ループ部の事前条件，事後条件，不逆ポーランド記法の数式の値を計算するという処理内

変式ごとの適合率の平均を比較すると同程度になっ

容が他のプログラムに比べて複雑であるために変数のた．また，再現率，F 値に関しても同様の結果が得ら値を監視するだけでは正しい表明を生成しにくかった

れた．Daikon がプログラムに対して表明を生成できためと考えられる．他のプログラムは入力，出力デーるのはメソッド部に限られているために，直接ループタともに int 型の配列変数であり変数の値の監視だけ部に対して事前条件，事後条件，ループ不変式を生成で必要な表明を生成しやすいと考えれられる．

することはできない．そこで，本稿では，ループ部を

表 3 の適合率は表 2 に比べ低下している．本研究で抽出し新たなメソッドとし，このメソッドに対して表は再現率も人手により求めている．これらの結果は，

明を生成することでループ部の事前条件，事後条件を適合率，再現率をともに ESC/Java2 の判定により求生成した．また，ループ内に空のメソッドを追加し，めた既存の結果 [3] と比較するとかなり悪い．これは，このメソッドに対して表明を生成することでループ不ESC/Java2 としては正しいが人間がみて不要と思わ変式を生成した．このため，ループ部の事前条件，事れる表明が大量にでたことが理由である．このこと

後条件の適合率，再現率，F 値はメソッド部のものとから，ESC/Java2 による表明の判定よりも人手によ同程度になると考えられる．実験の結果得られた適合る判定の方が厳しいと言える．なお，結果は紙面の関率，再現率，F 値は全体的に低いという結果になった

係上記載しないが，メソッドの事前条件と事後条件でが，Daikon を実際に利用する上での課題がわかったは，事後条件の方が適合率，再現率ともに事前条件のという点で意味があると考えられる．また，Daikonものより良くなる傾向があった．以上の結果をまとめはそもそも事前条件，事後条件の生成が主目的であると，現段階での Daikon が生成した表明の妥当性はり，ループ不変式は比較的考慮されていない．そのた

ESC/Java2 で機械的に計測した場合，メソッド，ルーめ，Daikon をループ不変式生成に使えるか否かの評

プ部ともに同程度である．しかし，適合率を人手で判価も必要となる．結果として，表 2 に示したループ部定した場合，ESC/Java2 で適合率を求めた場合に比の適合率，再現率は文献 [4] のものより低くなること

べ，表明の F 値は表 3 に示したように総じて低く妥当が分かった．適合率の低下の原因として，メソッドと性はメソッド，ループ部ともに十分とは言えない．妥

ループ部の表明を求める際に考慮すべき条件の違いが当性を高めるためには適合率，再現率の向上が必要で

2

レター
表2

ループ部における適合率，再現率，F 値
Table 2 The results of loop parts

No.
123456P
0.76
0.87
0.88
0.92
0.90
0.94

Loop
R
0.29
0.57
0.67
0.64
0.56
0.46

2002, pp. 234–245, 2002.
[5]G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: a behavioral interface specification language for java. ACM SIGSOFT, Vol. 31,

F
0.41
0.69
0.76
0.76
0.69
0.62

No. 3, pp. 1–35, 2006.

（平成 xx 年 xx 月 xx 日受付）

表 3 人手で求めた適合率
Table 3 Metrics evaluated by human
No.
1
2
3
4
56

P
0.22
0.50
0.05
0.06
0.07
0.11

MethodRF0.20 0.29
0.20 0.21
0.20 0.08
0.40 0.10
0.20 0.10
00P
0.53
0.43
0.56
0.28
0.15
0.13

LoopR
0.29
0.57
0.67
0.64
0.56
0.46

F
0.37
0.49
0.61
0.39
0.23
0.20ある.

5. あ と が き
本研究では，ループ構造が主体となり，アルゴリズムの実装が主となる比較的小規模のプログラム群に対して Daikon が生成した表明の適合率を ESC/Java2による判定と人手による判定の 2 通りの方法で求めた．
その結果，適合率は ESC/Java2 による判定では高いが，人手による判定では低いことを確認した．今後の課題として，表明自動生成の観点から，必要な表明の生成精度の向上，無駄な表明の削除が挙げられる．これらを解決するためには表明の生成，削減手法の改善だけでなく，テストケースの作成方法の改良が必要である．また，静的解析と Daikon の動的解析を組み合わせるということも考えられる．
文

献

[1]

B. Meyer.

Object-Oriented Software Construction[2]

M. D. Ernst, J. H. Perkins, P. J. Guo, S. Mccamant,

2nd Ed. Prentice-Hall, 2000.
C. Pacheco, M. S. Tschantz, and C. Xiao. The daikonsystem for dynamic detection of likely invariants. Science of Computer Programming, Vol. 69, No. 1-3,pp. 35–45, 2007.
[3]

J. W. Nimmer and M. D. Ernst. Automatic generation of program specifications. in Proc. of the 2002
Int. Symp. on Software Testing and analysis (ISSTA), pp. 232–242, 2002.

[4]

C. Flabagan, K. Rustan, M. Leino, M. Lillibridge,G. Nelson, J. B. Saxe, and R. Stata. Extended static
checking for java.

Proc. of the ACM SIGPLAN3Abstract For given Java programs, Daikon produces pre- and post-conditions with high recall andprecision when these metrics are evaluated with ESC/Java 2. The paper shows recall and precision ofassertions including loop invariants produced by Daikon for small programs. The metrics are evaluated byboth ESC/Java2 and human power. The results show that the metrics by human are less than those byESC/Java 2. The paper also gives the reason and discussions on it.
Key words Java, Pre-condition, Post-condition, Invariant, Daikon, JML, ESC/Jsva2