Detail of a work
小林和貴, "ESC/Java2の反例出力を利用したJavaメソッド実行パス取得ツールの試作および評価," , 2010年2月.
ID 113
分類 学位論文
タグ ESC/Java2
表題 (title) ESC/Java2の反例出力を利用したJavaメソッド実行パス取得ツールの試作および評価
表題 (英文)
著者名 (author) 小林和貴
英文著者名 (author) Kazuki Kobayashi
キー (key) Kazuki Kobayashi
刊行月 (month) 2
出版年 (year) 2010
刊行形式 (howpublished)
URL
付加情報 (note)
注釈 (annote)
内容梗概 (abstract) オブジェクト指向ソフトウェアの設計における，Design by Contract(DbC)はプログラムにおける仕様をソースコード中に記述することにより，ソフトウェア開発における誤りの箇所を明確にする手法である．

プログラムのソースコード中に事前条件・事後条件・不変条件などをアサーションという形で記述し，
静的解析ツールESC/Java2を用いて検証することができる．
これによりプログラムの保守性や信頼性を向上することができる．
しかしながら，アサーションをすべて人手で記述するにはコストが掛かるという問題点がある．
これを解決するために，テストケースを用いることによりアサーションの自動生成をするツールDaikonがあるが，
生成されるアサーションの品質はテストケースの品質に依存するという問題点がある．
また，あらかじめ用意されたルール以外のアサーションを自動生成することは困難である．
一方，すでに作成したソースコードに対しアサーションを人手で記述する場合，
必要な仕様記述が漏れてしまう事が考えられ，
プログラムに対する静的解析が不十分となる可能性がある．

そこで，本研究では，アサーション記述を支援するため，メソッドの実行パスの情報を提示する手法の提案を基にツールの実装を行った．
本ツールは，対象プログラムのメソッドに対して，
実行可能性のあるパスをプログラム依存グラフ(PDG)を利用して導出したのち，
ESC/Java2の反例出力機能を利用し，
アサーション記述や静的解析に必要な，メソッドの実引数に関する条件式や内部変数に関する条件式を提示し，
テストケースの雛形を提示する．

ツールの出力の妥当性を検証するため，いくつかのJavaソースコードに対してツールを適用した結果，
有用なテストケース制約式を得られることを確認した．
さらに，ツールの出力を用いてDaikonのテストケースを作成し，アサーションを自動生成した結果，
いくつかの正しいアサーションを導出することができた．

論文電子ファイル soturon.pdf (application/pdf) [一般閲覧可]
BiBTeXエントリ 
@misc{id113,
         title = {ESC/Java2の反例出力を利用したJavaメソッド実行パス取得ツールの試作および評価},
        author = {小林和貴},
         month = {2},
          year = {2010},
}