概要: Design by Contract に基づく表明の記述はソースコードの仕様理解の補助やプログラム の検証に役立つ．しかし，ソースコードのサイズの増加に伴い，表明の記述量も増大する．そのため，表明の自動生成手法が注目されている． 表明の自動生成手法には静的生成手法と動的生成手法が存在する．表明の静的生成手法では，プログラムを静的に解析することで，表明を導出する．しかし，表明生成にかかる時間が長い点が問題となる．表明の動的生成手法では，テストケースを用いて引数やフィールド変数の値を変えながら対象メソッドを解析し，データを取得する．それにより，比較的少ないコストで表明を生成できる．代表的な表明の動的生成ツールにDaikon などがある． 一方で，表明の動的導出手法はテストケースにの質が生成表明に影響を与えるという問題がある．ここでテストケースとの質とは，テストケースがどれだけの実行範囲をカバーしているかを表す．この問題に対し，インバリアントカバレッジという指標が存在する．インバリアントカバレッジとはテストケースがどれだけプログラムの返り値にデータ依存関係を持つ命令文を実行するかを表す指標である．著者が所属する研究グループではインバリアントカバレッジの値が高いテストケースを静的解析器ESC/Java2 の反例出力を用いて導出する手法を提案してきた． しかし，既存研究では導出したテストケース制約が本来求めるべき制約より狭いという課題点があった．これは既存研究では反例情報に基づいたテストケース制約の導出を行っているため起こる問題である． 提案手法ではSMT ソルバを用いてこの課題を解決する．まず，対象メソッドのPDG からインバリアントカバレッジを満たす実行パスを列挙する．その実行パスをSMT ソルバの文法に変換し，求解する．その解を用いて，そのパスの実行可能性と具体的な引数値を導出する．提案手法を複数のJava プログラムに対して適用し，評価実験を行った．その結果，提案手法が有用であることを確認した． タグ: assertion, Invariant, coverage, SMT, solver, PDG, Daikon

@mastersthesis{佐々木幸広2012,
  author = {佐々木 幸広},
  title = {Java の実行パスからパス実行可能性判定式への変換と SMTソルバによる求解},
  school = {大阪大学},
  type = {Bachelor's Thesis},
  year = {2012},
  month = {feb}
}