|
ソフトウェアの精密な検証について以下の研究を行った。
1)アルゴリズム検証の事例研究として、重み付きグラフに対して最短経路を求めるBellman-Fordアルゴリズムの形式化及び検証を行った。アルゴリズム教科書では、重みとして実数など具体的な代数構造を仮定してアルゴリズムの形式化が行われる。一方、本研究では、必要最低限の性質を仮定し形式化を行った。代数的な構造としてどのような性質が必要かを、厳密な証明をすることで明確にすることができた。また、グラフの経路の形式化をリストの構造に対応するように行うことで、グラフアルゴリズムの形式化が扱いやすくなることが分かった。
2)プログラム検証の事例研究として、KMP法による文字列照合のC言語による実装の正しさを検証した。検証には、検証条件生成ツールCaduceusを用いた。ループ不変条件を決定するには、プログラムの精密な分析が必要であったが、検証条件の証明自体は、比較的容易であった。また、検証の過程でアルゴリズムの教科書に掲載されているC言語によるKMP法の実装の誤りを発見することができた。
3)Cプログラムに対する検証条件生成ツールCaduceusの最新版を定理証明系Isabelleに対応させる実装を行った。この実装に基づき、Caduceusの解説をコンピュータソフトウェア誌に書いた。Caduceusによる検証の原理から、配列及びポインタを用いたプログラムの検証までを解説した。
|
