氏名: 寺澤 啓司 (289834252)

論文題目: オブジェクト指向計算モデルにおける例外処理の形式化


論文概要

オブジェクト指向言語を形式化したobject calculusは、 命令型操作意味論と型システムを持ち、 コンパクトで表現能力が豊かな計算モデルであり、 オブジェクト指向言語の設計や理解に有用である。 Javaなどのオブジェクト指向言語の多くの機能は このobject calculusで表現することができるが、 計算の途中で例外が発生したときに、計算を止めて例外処理に移るような 例外処理機能を表現することができない。

そこで本研究では、object calculusに 処理する例外を型によって指定できる 例外処理の機能を加えて拡張する。 このような例外処理機能は、処理する例外を型によって取捨選択するという Javaの例外処理機能を形式化したものになっている。 従って、拡張したobject calculusに基づいて、 例外処理を含むJavaプログラムを解析することが可能となる。

object calculusの拡張の要点は次のとおりである。 まず、例外を発生させるthrow構文と、 処理する例外を型によって指定できる例外処理構文try catchを追加する。 次に、操作意味論と型システムを拡張する。

操作意味論は各構文の評価結果と、 その結果を得るために必要な条件からなる規則によって定義される。 throw構文で発生される例外を表すオブジェクトを 通常のオブジェクトと区別して扱い、 try catch構文で例外処理を行うか行わないかを判断する。 発生した例外の型が指定された型のサブタイプである場合は例外処理に移り、 サブタイプでない場合は例外処理を行わない。 このような動作を全て規則によって定義する。 サブタイプであるかどうかの判定には、 2つの型がサブタイプの関係であることを判定する規則と、 2つの型がサブタイプの関係でないことを判定する規則を使用する。 このため、 2つの型がサブタイプの関係でないことを判定する判定規則を新たに導入する。 また、例外が発生した場合に、処理されるまで通常の計算を止めるための規則 の追加も行う。

起こりうる例外の型を列挙したような例外付きの型を用いて、 型システムの拡張を行う。 例外付きの型同士がサブタイプかどうかを判定する規則や、 throw構文やtry catch構文の型を判定する規則を追加する。 この拡張によって、型検査を行うことで、 どのような例外が起こり得るかを調べることができる。

以上のように拡張したobject calculusに対して、 サブタイプでないことの判定規則の健全性を示す。 また、操作意味論の型に関する健全性について検討する。


目次に戻る


asakura@nuie.nagoya-u.ac.jp