概要: Design by Contract に基づく表明の生成手法には静的生成手法と動的生成手法が存在する．動的生成手法では，テストケースを用いて引数やフィールド変数の値を変えながら対象メソッドを解析し，データを取得するため，比較的少ないコストで表明を生成できる．一方で，テストケースがどれだけの実行範囲をカバーしているかというテストケースの質が生成される表明の質に影響を与える．この問題に対し，インバリアントカバレッジという指標が存在する．本研究では対象メソッドのPDG からインバリアントカバレッジを満たす可能性のある実行パスを列挙しSMTソルバを用いてそのパスの実行可能性と具体的な引数値の導出を行う方法を提案する．また，複数の例題に適用し有効であることを確認した． タグ: SMT, solver, PDG, Daikon, test, case, Java

@inproceedings{佐々木幸広2012a,
  author = {佐々木 幸広 and 小林 和貴 and 岡野 浩三 and 楠本 真二},
  title = {SMTソルバーとPDG作成ツールを用いた Java のテストケース自動導出手法の提案},
  booktitle = {電子情報通信学会技術研究報告},
  volume = {111},
  number = {481},
  pages = {55--60},
  year = {2012},
  month = {feb}
}