| 研究概要 |
H21年度は、H20年度までに開発した形式仕様・証明スコアとそれらの解析結果に基づき、問題モデルの検証技術に関し、以下の2つの成果を得た。
1.証明スコア法の完全性に関する理論的成果:
CafeOBJ言語による証明スコア法の基本操作は、(1)帰納法、と(2)場合分け、の適用である。これらの操作(1),(2)が健全(sound)、つまり論理的に正しいものである、ことは検証法であるための必要条件である。一方、操作(1),(2)が検証操作としで完全(complete)、つまり検証可能な命題は操作(1),(2)により検証できる、ことは検証法が持つことが望ましい性質ではあるが、この性質を有する検証法は稀である。我々は、証明スコア法が完全であることを理論的に示した。この結果は、CafeOBJ仕様に基づく証明スコア法が、つ極めて強力な検証法であることを示すものである。
2.証明メコア法と探索法を組み合わせた検証法に関する方法論的な成果
証明スコア法は対話的検証法であり、その一部を自動化して検証の自動化率を向上することは本基盤研究の最大の目標の一つであった。(1)無限状態を有限状態に帰着させる抽象化の正しさを証明スコア法で検証し,(2)有限状態については全ての場合を探索ツールで網羅的調べる、ことで無限状態に対する検証を行う方法を発見し、定式化した。
以上の1と2の成果のうち、1の理論的な成果は当初は予想しなかったものであるが、かなり一般的な形で証明スコア法の完全性を保証する理論的な成果を得ることが出来た。2は年度当初に計画したとおりの成果であり、4年間の本基盤研究の成果の中でも最も重要なものの一つである。これら2つの成果は、それらに基づきさらに強力な問題モデル検証技術を構築できる可能性があり、今後の発展が期待できる。
|
