| 研究概要 |
本研究はソフトウェアの自動デバッグ方式の構築を目的とし,特にプログラムの誤り特定手法の開発に重点を置く.そのためのアプローチとして制約の概念を採用する.具体的には,事後条件違反を生じる入力をモデル検査によって求め,入力,プログラム,事後条件から制約充足問題を構成した上で,違反の原因となった制約を特定し,プログラム中の対応する部分を誤り箇所の候補として提示する.本研究では効果的な誤り特定を行うために,特に柔らかい制約の考え方を採用する.またこの方法を応用して誤りの修正候補の提示も実現する.本研究ではこのような柔らかい制約を用いた自動デバッグ方式を構築し,C言語を対象とする自動デバッグツールを開発する.
初年度である平成24年度には,特に制約処理手法の高度化に関する研究を行った.従来の研究ではプログラムの誤り特定のために主に充足可能性判定の手法が使われていたのに対して,本研究では制約プログラミングの手法を採用していることが特徴である.充足可能性判定の手法でも算術的な式を論理式に変換することで扱うことができるが,一般に論理式による算術式の表現は単純ではなく,C言語で書かれたプログラムを変換すると問題が大きくなる.一方,制約プログラミングでは論理式による内部表現を用いることなく,算術式を含む問題を扱うことができる.しかし,C言語のプログラムには論理式が含まれることも多くあり,従来の制約プログラミングの手法は逆にそのような場合に適していない.本研究では制約プログラミングによって算術式と論理式の両方に適切に対処し,さらに柔らかい制約として処理することのできる手法を構築した.
|
