| 研究概要 |
本研究の目的は,オブジェクト指向プログラムの実行中に発生する例外がもれなく処理されるか否かをプログラムの実行前に検査するための原理を明らかにすることである.これまでの研究で,例外処理機能を追加した単純なオブジェクト指向計算モデルに対して,例外発生の可能性を型として扱うための型システムを提案し,その健全性を証明している.本研究の具体的目標は,単純なオブジェクト指向計算モデルの場合の型推論アルゴリズムを開発すること,および,項書換え系の逆計算技法を用いた高機能なモデルに対する型推論手法を与えることである.
今年度は,例外処理付きオブジェクト指向プログラムの安全性について研究を行なった.この研究では,文がスローし得る例外の集合と文に出現する情報流のあるデータの機密度からなる安全型と型システムを導入し,その型システムが非干渉性に対して健全であることを証明した.また,項書き換え系の停止性,木オートマトンにおける到達可能性,動的型付き関数型言語のソフトタイピング等の研究を実施した.これらの研究を統合して,オブジェクト指向プログラムや並行分散プログラムの安全性の解析に応用することは今後の課題として残った.
|
