| 研究実績の概要 |
本研究の大目標は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装することであった. 研究成果は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して,再帰呼出しを追加した論理体系をまず構築し, これをほぼ実装した. このために, 配列のある記号ヒープのエンテイルメントの判定器の理論を構築し, この判定器の正当性性を証明し, パソコン上に実装して実験を行い, 理論の有効性を示した. また, Cプログラムからプログラムの同等性を保って関数ポインタを除去するアルゴリズムを提案し, これをパソコン上に実装して実験を行い, アルゴリズムの有効性を示した.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して,再帰呼出しを追加した論理体系をまず構築し, これをほぼ実装した. このために, 配列のある記号ヒープのエンテイルメントの判定器の理論を構築し, この判定器の正当性性を証明し, パソコン上に実装して実験を行い, 理論の有効性を示した. また, Cプログラムからプログラムの同等性を保って関数ポインタを除去するアルゴリズムを提案し, これをパソコン上に実装して実験を行い, アルゴリズムの有効性を示した. また配列とリストをもつ分離論理における両仮説形成アルゴリズムを提案し, その正当性を証明し, これをパソコン上に実装して実験を行った. 以上により進捗はおおむね良好であるといえる.
|
| 今後の研究の推進方策 |
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装する研究をさらに進める.ループ解析の精度が必要であることがわかってきたので, 抽象解釈の技法を取り入れてループ解析を高精度化する.
|
