| Outline of Annual Research Achievements |
本研究の目的は, オハーン理論を発展させることにより高精度なソフトウェア検証を可能にする新理論を構築することであった. 研究成果は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系をまず構築し, さらにこれに対して改良を続けて, 結果として得られた論理体系に対して定理証明, 両仮説形成, 記号計算のループインバリアント生成のアルゴリズムを与えた. また, この論理体系に基づいた実装システムをパソコン上に作成し, これを用いていくつかのプログラムの安全性を検証した. 具体的には, 分離論理を一般帰納的述語, 配列, 算術により同時に拡張する研究をさらに進めた. まず, 同時に拡張した論理体系を定義し, 次に, その論理体系に対して, 定理証明, 両仮説形成, 記号計算のループインバリアント生成の三つを計算する効率よいアルゴリズムを与え, アルゴリズムを実装した. また, それらのアルゴリズムの正しさおよび決定可能性を数学的に証明し, またそれらのアルゴリズムの効率を実装を用いた実験により証拠付けた. また, 一般帰納的定義を扱うシステムだけではなく, 一般帰納的定義のうちで実際のソフトウェア検証によく現れるリストを特別に高速に扱えるシステムの研究も行った.
|
