書換え技術に基づくソフトウェア解析

点击翻译按钮获取中文摘要

CafeOBJ, Maude, OBJ3などの高級仕様記述言語で書かれたプログラムでは、戦略アノテーションにより評価戦略をユーザが明示的に制御できる。戦略アノテーションの付いたプログラムは、停止性が特定の条件下で、文脈依存書換えの最内停止性と同値になることが、Lucasにより証明された。また、これまでに文脈依存書換え系の停止性を通常の項書換え系の停止性へ帰着させる、書換え系間の変換がいくつか提案されている。しかし従来の変換は、文脈依存書換え系の最内停止性を証明ためには十分といえるものではなかった。我々は、最内停止性に対し健全かつ完全であるような新たな変換方法を開発した。この変換を用いれば、文脈依存書換え系における最内停止性は、変換後の書換え系の最内停止性に帰着できる。項書換え系の最内停止性は停止性に比べ、自動証明を容易に行える。停止性を保証する問題は計算機科学の多くの分野で生じる。項書換え系に対する停止性の研究は数十年に渡り行われ、数多くの強力な手法が開発されてきた。近年、依存対法と呼ばれる新たな手法がArtsとGieslにより開発された。この手法では、書換え系を不等式で表される制約式の集合へ変換する。書換え系の停止性はこの制約式が解を持つことと同値になる。変換前の書換え系が、多項式解釈や経路順序などの標準的な手法では停止性を証明できない場合でも、変換後は証明可能になる。我々は、木オートマトンを用いることによって、依存グラフのよりよい近似を求めることができ、依存対法が改良されることを証明した。よりよい近似グラフが得られれば、制約条件が緩和され、停止性の証明が容易になる。現在、この理論に基づく依存対法の実装に取り組んでいる。