| 研究概要 |
本研究の目的は,オブジェクト指向プログラムの実行中に発生する例外がもれなく処理されるか否かをプログラムの実行前に検査するための原理を明らかにすることである.これまでの研究で,例外処理機能を追加した単純なオブジェクト指向計算モデルに対して,例外発生の可能性を型として扱うための型システムを提案し,その健全性を証明している.本研究の具体的目標は,単純なオブジェクト指向計算モデルの場合の型推論アルゴリズムを開発すること,および,項書換え系の逆計算技法を用いた高機能なモデルに対する型推論手法を与えることである.
今年度は,並行分散プログラムの通信エラーの検査を型システムにより行う手法,通信の安全性を保証する方法としてカラーペトリネットを利用する手法,高階関数プログラムの停止性証明について研究を行った.
1.エージェントの移動機能を記述できる並行分散計算モデルJoin Calculusとオブジェクト指向言語Javaを融合した言語JoinJAVAを設計し,その処理系を開発した.また,プログラムの通信エラーを静的に検査するための型判定システムを与え,その健全性を証明した.
2.秘密の情報が第3者に知られないこと,すなわち,機密性は通信プロトコルの最も重要な性質の一つである.通信プロトコル記述言語で書かれたプロトコルをカラーペトリネットに変換し,プロトコルの機密性を変換で得られたカラーペトリネットの到達可能性問題に帰着する手法を与えた.この変換より,機密性の十分条件を判定できることを明らかにした.
3.項書換え系の停止性証明に用いられる辞書式経路順序を高階関数を扱う関数プログラムに適用できるように拡張する方法を3種類与え,様々な項集合でのそれぞれの拡張の性質を明らかにした.
|
