再利用性に優れた型付オブジェクト指向プログラミング言語の理論と設計

点击翻译按钮获取中文摘要

本年度は、Bruceらの提案するMyTypeとOwnership。typesやUniverse typesといったオブジェウト指向プロゲラミンゲ言語におけるカプセル化を制御するための型との関わりについて調査、研究した。MyTypeは、クラスの安全な再利用を目的とする型で、universe typesなどとは、関わのが薄そうに思えるかも知れないが、それらの使用パターンを調査してみると、実用的な範囲で類似性があることが分かった。このことは、プログラムに型を付けるにあたって、MyTypeとUniverse types別々に与えてやる必要がないことを意味し、1つの記述で、2種類の安全性に関わる性質が得られるようなプログラミング言語の開発に繋がり、重要な発見であると言える。この提案が正しいことを証明するために、形式的手法を使用した。形式的手法とは、提案するプロゲラミンゲ言語の極小モデルを作成し、その性質を数学的に厳密に証明する手法である.ここでは、MyTypeとUniverse typesの両方を含むJava言語の極小モデルを作成し、その文法、型付け規則、操作的意味論を与え、その性質として、型安全性定理、owner-as-modifier定理を証明した。これらの定理により、1つの記述により、2種類の安全性が同時に得られることが分かった。