| 研究概要 |
本研究の目的は,オブジェクト指向プログラムの実行中に発生する例外がもれなく処理されるか否かをプログラムの実行前に検査するための原理を明らかにすることである.これまでの研究で,例外処理機能を追加した単純なオブジェクト指向計算モデルに対して,例外発生の可能性を型として扱うための型システムを提案し,その健全性を証明している.本研究の具体的目標は,単純なオブジェクト指向計算モデルの場合の型推論アルゴリズムを開発すること,および,項書換え系の逆計算技法を用いた高機能なモデルに対する型推論手法を与えることである.
今年度は以下の研究を行った。
1.オブジェクト指向計算モデルのプログラムが与えられたとき,そのプログラムの型を推論するアルゴリズムを与え,実装を行った.この型推論アルゴリズムにより,与えられたプログラムの型が分かり,その型から例外処理洩れの有無が判定できる.
2.上記の型推論アルゴリズムをJavaプログラムの例外処理洩れ検査に応用する手法を開発した.具体的には,例外処理にのみ焦点を絞ってJavaプログラムをオブジェクト指向計算モデルのプログラムに変換し,変換後のプログラムの型推論を行うことで,Javaプログラムの例外処理洩れを検査する方法である.
3.項書換え系の逆計算に関しては,構成子項書換え系というクラスに対して,与えられた項書換え系の逆計算を行う項書換え系を生成するアルゴリズムを与え,その正当性を証明するとともに,逆計算項書換え系の計算が効率良く行えるための条件を明らかにした.また,高階項書換え系に関して停止性判定法および帰納的定理の特性化を与えた.
|
