| 研究概要 |
関数型プログラムの等価性は,リダクション関係の等価性を示すことで形式的に検証できる.このような等価性の検証はプログラム変換の正当性を保証するために不可欠であるが,実際のプログラムの等価性は,木やリストなどのデータ構造上の関数の帰納的な性質に基づいて示す必要があるため,単純なリダクション関係のみを解析しても検証は困難である.
本研究では,プログラム変換の多くが抽象化された変換パターンとして一般化できることに注目し,変化パターンの等価性を保証する手法を明らかにした.具体的には,プログラムによる具体的な計算過程をプログラムパターンによる抽象的なリダクションによって近似し,プログラムを構成する関数の抽象的な性質のみに基づいて変換パターンの等価性を保証する手法を与えた.ここで開発した手法は,変換パターンの正当性を潜在帰納法に基づいて間接的に示すため,具体的なデータ構造に基づく帰納法を直接適用する必要はなく,これまで提案された手法と比較すると自動化に適している.
また,リダクションによる到達可能性を近似木オートマトンに基づいて解析する手法の検討を行った.さらに,プロトコルの安全性を判定する近似木オートマトンを実装し,リダクションの近似に基づくセキュリティ性解析の実験を行った.
|
