本論文の研究の主な目標は、inner classと呼ばれるJavaの入れ子クラス機構とGJの型抽象機構の型システム、コンパイル技法の本質的な仕組みを明らかにすることにある。 本論文は7章から成り立っている。第1章においては、本研究の背景であるクラスに基づくオブジェクト指向プログラミングと、先進的なクラス機構について紹介されている。オブジェクト指向プログラミングにおいては、C++やJavaに代表されるクラスを用いたオブジェクト指向言語が主流となっている。クラスの基本的な機能は、同様の動作をするオブジェクトを簡潔に記述することである。最近の言語には、この基本的な機能に加えて、BetaやJava1.1で見られる入れ子クラス、またはC++のテンプレートや、Bracha,Odersky,Stoutamire,Wadlerの提案によるGJなどのいくつかのJavaの拡張に見られる、クラスの型抽象などの様々な先進的な機構が採り入れられている。入れ子クラスは入れ子関数/手続きに似たプログラミングを可能にし、型抽象はリストなど多相型データ構造の表現をより簡便にする。しかし、これらの機構は非常に複雑であるため、プログラムの振る舞いを理解することが困難になっている。 第2章において、inner classおよびGJのモデルを構築するための基礎として、Featherweight Javaと呼ぶ、クラスに基づくオブジェクト指向言語のための小さな核言語が定義され、その型安全性などの性質を証明されている。Featherweight Javaは、複雑な拡張機能に関する証明が扱えるように、クラスに基づく言語の必要最小限の機能のみをとらえた言語として設計さている。 第3章においてinner classの主要部分の形式化と型安全性の証明が行われいる。Featherweight Javaがinner classにより拡張されている。意味論の定義を通じてinner c1assと継承機構の相互作用に関する複雑さが明らかになった。 第4章と第5章においてGJの型抽象機構の形式化と型安全性の証明が行われている。特に第4章においてはGJのコンパイル技法の形式化と正当性の証明が行われている。拡張言語からFeatherweight Javaへの変換規則を与えることによりコンパイラをモデル化し、その変換が型付けと意味論を保存することが証明された。 第5章においては、Featherweight JavaがGJの特徴的な機構であるraw typeによって拡張されている。raw typeは多相型クラスとその古い単相型バージョンを使おうとする古いクライアントとの互換性を保つために設計された機構である。raw typeの型安全性に関する証明を通じて現在のraw typeの設計の欠陥、仕様の不備などが明らかになった。 第6章では関連研究、第7章では結論が述べられている。 なお、本論文は、Benjamin Pierce氏、Philip Wadler氏との共同研究に基づいているが、論文提出者が主体となって分析及び検証を行なったもので、論文提出者の寄与が十分であると判断する。 従って、博士(理学)を授与できると認める。 |