2006 Fiscal Year Annual Research Report
書換えに基づく例外型を持つオブジェクト指向プログラムの型推論
| Project/Area Number |
16300005
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
坂部 俊樹 名古屋大学, 大学院情報科学研究科, 教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
酒井 正彦 名古屋大学, 大学院情報科学研究科, 教授 (50215597)
草刈 圭一朗 名古屋大学, 大学院情報科学研究科, 准教授 (90323112)
西田 直樹 名古屋大学, 大学院情報科学研究科, 助教 (00397449)
|
|---|
| Keywords | オブジェクト指向計算 / 例外処理 / 通信エラー / 機密性 / 型推論 / 項書換え系 |
|---|
| Research Abstract |
本研究の目的は,オブジェクト指向プログラムの実行中に発生する例外がもれなく処理されるか否かをプログラムの実行前に検査するための原理を明らかにすることである.これまでの研究で,例外処理機能を追加した単純なオブジェクト指向計算モデルに対して,例外発生の可能性を型として扱うための型システムを提案し,その健全性を証明している.本研究の具体的目標は,単純なオブジェクト指向計算モデルの場合の型推論アルゴリズムを開発すること,および,項書換え系の逆計算技法を用いた高機能なモデルに対する型推論手法を与えることである.
今年度は,例外処理機能を持つオブジェクト指向プログラミング言語で記述されたプログラムが機密情報を保護することを検証するための型システムについて研究を行い,以下の成果を得た.
例外処理による情報流は,スローされる例外とそれを捕捉する箇所に依存して変化する.この情報流を解析するためには,プログラム中の各文についてどの例外からの制御依存が存在するか把握しなければならない.そこで,文の情報流に影響されるデータの最小の機密度と文がスローしうる例外の集合から成る安全型を導入し,この安全型に基づいて従来の型システムを拡張した.本型システムは,プログラムの安全性を表す非干渉性に対して健全であることを示した.
その他,手続き型プログラムを項書換え系に変換してプログラムの性質を検証擦る方法,等式と項書換え系の対で与えられる計算システムにおける等式削減手法,条件付き項書換え系から項書換え系を得るための紐解変換に関する研究成果を得た.
|
