| 研究概要 |
本研究の目的は,オブジェクト指向プログラムの実行中に発生する例外がもれなく処理されるか否かをプログラムの実行前に検査するための原理を明らかにすることである.これまでの研究で,例外処理機能を追加した単純なオブジェクト指向計算モデルに対して,例外発生の可能性を型として扱うための型システムを提案し,その健全性を証明している.本研究の具体的目標は,単純なオブジェクト指向計算モデルの場合の型推論アルゴリズムを開発すること,および,項書換え系の逆計算技法を用いた高機能なモデルに対する型推論手法を与えることである.
今年度は,例外処理機能を持つオブジェクト指向プログラミング言語で記述されたプログラムが機密情報を保護することを検証するための型システムについて研究を行い,以下の成果を得た.
例外処理による情報流は,スローされる例外とそれを捕捉する箇所に依存して変化する.この情報流を解析するためには,プログラム中の各文についてどの例外からの制御依存が存在するか把握しなければならない.そこで,文の情報流に影響されるデータの最小の機密度と文がスローしうる例外の集合から成る安全型を導入し,この安全型に基づいて従来の型システムを拡張した.本型システムは,プログラムの安全性を表す非干渉性に対して健全であることを示した.
その他,手続き型プログラムを項書換え系に変換してプログラムの性質を検証擦る方法,等式と項書換え系の対で与えられる計算システムにおける等式削減手法,条件付き項書換え系から項書換え系を得るための紐解変換に関する研究成果を得た.
|
