Formalizing Advanced Class Mechanisms

By Atsushi Igarashi. PhD thesis, Dept. of Information Science, University of Tokyo, March 2000.

Abstract

Class-based languages, such as C++ and Java, form the mainstream of object-oriented programming. The basic function of classes is to describe objects with similar behavior concisely. Recent languages have added to the basic class mechanism a variety of advanced features, such as inner classes, found in Beta and in Java 1.1, and type parameterization of classes, found in C++ as templates and in several extensions for Java, including GJ [Bracha, Odersky, Stoutamire, and Wadler]. Inner classes enable a programming style similar to nested functions/procedures, while type parameterization makes programming of polymorphic data structures, such as lists, more convenient. However, this power comes at a significant cost in complexity, which makes it difficult to understand the behavior of programs.

The main goal of this work is to clarify the essence of the type systems and compilation schemes of inner classes and GJ-style type parameterization. We approach this goal by building their formal models based on a small core calculus, called Featherweight Java, for class-based object-oriented languages, and by proving their properties, such as type soundness. Our contributions are as follows.

Design and formalization of Featherweight Java. It is intended to be a smallest possible language to capture the essential parts of type systems of class-based object-oriented languages, so that proofs for the complex extensions are tractable.
Formalization of the core of inner classes and proof of its type safety. Featherweight Java is extended with inner classes; the definition of its semantics illuminates complexity related to interaction between inner classes and inheritance.
Formalization of the core of GJ and proof of its type safety. We extend Featherweight Java with type parameterization and raw types, one of GJ's distinctive features. Raw types are designed to maintain compatibility between polymorphic classes and their legacy clients that still expect the old monomorphic version of those classes. The proof of type soundness of raw types uncovers some underspecifications and flaws in the current design of raw types.
Formalization and proof of correctness of the compilation schemes of inner classes and GJ. We model the current compilers by giving translation from the extended languages into Featherweight Java, and prove that the translation preserves well-typedness and semantics.

PostScript file

thesis.ps.gz (503kbytes.)
thesis-en.ps.gz (447kbytes; the Japanese title and abstract are excluded.)