オブジェクト指向分析モデルの定理証明系を用いた検証支援に関する研究

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

平成13年度は、前年度作成した検証支援環境F-Verifierを用いて実験、及び実験結果の解析を行った。F-Verifierでは、図形エディタで作成したオブジェクト指向分析モデルを、定理証明系HOLで取り扱い可能な形式に自動変換する。そして、HOL上で対話的証明を行うことにより、構築した分析モデルの検証を行う。本年度は、図書館業務支援システムの分析モデルを作成し、F-Verifierを用いていくらかの性質に関して検証を行った。その結果、HOL上での対話的証明にかかるコストが問題であることが判明した。そこで、この問題を解決する手法について考察した。対話的証明のコストが高くなっていた理由は、分析モデルのHOLによる表現として用いているデータ型が原始的であるためであった。そのため、証明の際、粒度の細かい定理や推論規則を適用することになり、非常に多くの推論ステップを費やすことになった。この問題点を解決するためには、高級なデータ型をあらかじめ作成しておき、それを用いて分析モデルを作成することが有効である。このような高級なデータ型を作成する活動は、システム開発において対象領域に出現する概念を整理することに対応しており、領域分析手法と連携することにより効果的な手法となりうる。そこで、本年度は、図書館業務支援システムの分析モデルに出現するデータ型の抽象度を上げる実験も行った。その結果、前年度までに作成した公理系を拡張する必要があることが判明した。公理系の拡張に関しては今後の課題である。