On inner classes.
Inner classes in object-oriented languages play a role similar to nested function definitions in functional languages, allowing an object to export other objects that have direct access to its own methods and instance variables. However, the similarity is deceptive: a close look at inner classes reveals significant subtleties arising from their interactions with inheritance. The goal of this work is a precise understanding of the essential features of inner classes; our object of study is a fragment of Java with inner classes and inheritance (and almost nothing else). We begin by giving a direct reduction semantics for this language. We then give an alternative semantics by translation into a yet smaller language with only top-level classes, closely following Java's Inner Classes Specification. We prove that the two semantics coincide, in the sense that translation commutes with reduction, and that both are type-safe.
Introduction
It has often been observed that the gap between object-oriented and functional programming styles is not as
large as it might first appear; in essence, an object is just a record of function closures. However, there are
differences as well as similarities. On the one hand, objects and classes incorporate important mechanisms
not present in functions (static members, inheritance, object identity, access protection, etc. On the other
hand, functional languages usually allow nested definitions of functions, giving inner functions direct access
to the local variables of their enclosing definitions.
A few object-oriented languages do support this sort of nesting. For example, Smalltalk [3] has special
syntax for "block" objects, similar to anonymous functions. Beta [8] provides patterns, unifying classes
and functions, that can be nested arbitrarily. More recently, inner classes have been popularized by their
inclusion in Java 1.1 [6].
Inner classes are useful when an object needs to send another object a chunk of code that can manipulate
the first object's methods and/or instance variables. Such situations are typical in user-interface
programming: for example, Java's Abstract Window Toolkit allows a listener object to be registered with
a user-interface component such as a button; when the button is pressed, actionPerformed method of the
listener is invoked. For example, suppose we want to increment a counter when a button is pressed. We
begin by defining a class Counter with an inner class Listener:
class Counter -
int x;
class Listener implements ActionListner -
public void actionPerformed(ActionEvent e) - x++; -
void listenTo(Button b) -
b.addActionListener(new Listener());
In the definition of the method actionPerformed, the field x of the enclosing Counter object is changed.
The method listenTo creates a new listener object and sends it to the given Button. Now we can write
Counter new Counter();
new Button("Increment");
to create and display a button that increments a counter every time it is pressed.
Inner classes are a powerful abstraction mechanism, allowing programs like the one above to be expressed
much more conveniently and transparently than would be possible using only top-level classes. However, this
power comes at a significant cost in complexity: inner classes interact with other features of object-oriented
programming-especially inheritance-in some quite subtle ways. For example, a closure in a functional
language has a simple lexical environment, including all the bindings in whose scope it appears. An inner
class, on the other hand, has access, via methods inherited from superclasses, to a chain of environments-
including not only the lexical environment in which it appears, but also the lexical environment of each
superclass. Conversely, the presence of inner classes complicates our intuitions about inheritance. What
should it mean, for example, for an inner class to inherit from its enclosing class? What happens if a
top-level class inherits from an inner class defined in a different top-level class?
JavaSoft's Inner Classes Specification [6] provides one answer to these questions by showing how to
translate a program with inner classes into one using only top-level classes, adding to each inner class an
extra field that points to an instance of the enclosing class. This specification gives clear basic intuitions
about the behavior of inner classes, but it falls short of a completely satisfying account. First, the style
is indirect: it forces programmers to reason about their code by first passing it through a rather heavy
transformation. Second, the document itself is somewhat imprecise, consisting only of examples and English
prose. Different compilers (even different versions of Sun's JDK!) have interpreted the specification differently
in some significant details.
The goal of this work is a precise understanding of the essential features of inner classes. Our main
contributions are threefold:
ffl First, we give a direct operational semantics and typing rules for a small language with inner classes
and inheritance. The typing rules are shown to be sound for the operational semantics in the standard
sense.
To keep the model as simple as possible, we focus on the most basic form of inner classes in Java, omitting
the related mechanisms of anonymous classes, local classes within blocks, and static nested classes.
Also, we do not deal with the (important) interactions between access annotations (public/private/etc.)
and inner classes (cf. [6, 1]).
ffl Next, we give a translation from the language with inner classes to an even smaller language with
only top-level classes, formalizing the translation semantics of the Java Inner Classes Specification. We
show that the translation preserves typing.
ffl Finally, we prove that the two semantics define the same behavior for inner classes, in the sense that
the translation commutes with the high-level reduction relation in the direct semantics.
The basis of our work is a core calculus called Featherweight Java, or FJ. This calculus was originally
proposed in the context of a formal study [4] of GJ [2], an extension of Java with parameterized classes. It
was designed to omit as many features of Java as possible (even assignment), while maintaining the essential
flavor of the language and its type system. Its definition fits comfortably on a page, and its basic properties
can be proved with no more difficulty than, say, those of the simply typed lambda-calculus with subtyping.
This extreme simplicity makes it an ideal vehicle for the rigorous study of new language features such as
parameterized classes and inner classes.
The remainder of the paper is organized as follows. Section 2 briefly reviews Featherweight Java. Section 3
defines FJI, an extension of FJ with inner classes, giving its syntax, typing rules, and reduction rules, and
stating standard type soundness results. Section 4 defines a compilation from FJI to FJ, modeling the
translation semantics of the Inner Classes Specification, and proves its correctness with respect to the direct
semantics in the previous section. Section 5 offers concluding remarks.
For brevity, proofs of theorems are omitted; they will appear in a forthcoming technical report [5].
We begin by reviewing the basic definitions of Featherweight Java [4]. FJ is a tiny fragment of Java,
including only top-level class definitions, object instantiation, field access, and method invocation. (The
original version of FJ also included typecasts, which are required to model the compilation of GJ into Java.
They are omitted here, since they do not interact with inner classes in any significant way.) Since FJ is
a sublanguage of the extension defined in Section 3, we just show its syntax and an example of program
execution here. The rest of the definition can be found in Figure 4.
The abstract syntax of FJ class declarations, constructor declarations, method declarations, and expressions
is given as follows:
class C extends C -C f; K M-
e ::= x
new C(e)
The metavariables A, B, C, D, and E range over class names; f and g range over field names; m ranges over
method names; x ranges over parameter names; c, d and e range over expressions; L ranges over class
declarations; K ranges over constructor declarations; and M ranges over method declarations. We write f
as shorthand for f 1 ,. ,fn (and similarly for C, x, e, etc.) and write M as shorthand for M 1 . Mn (with no
commas). We write the empty sequence as ffl and denote concatenation of sequences using a comma. The
length of a sequence x is written #(x). We abbreviate operations on pairs of sequences in the obvious way,
writing "C f" as shorthand for "C 1 f 1 ,. ,Cn fn " and "C f;" as shorthand for "C 1 f 1 ;. Cn fn;" and
"this.f=f;" as shorthand for "this.f 1 =f 1 ;. this.f n =fn ;". Sequences of field declarations, parameter
names, and method declarations are assumed to contain no duplicate names.
A key simplification in FJ is the omission of assignment, making FJ purely functional. 1 An object's
fields are initialized by its constructor and never changed afterwards. Moreover, a constructor has a stylized
syntax such that there is one parameter for each field, with the same name as the field; the super constructor
is invoked on the fields of the supertype; and the remaining fields are initialized to the corresponding
parameters. (These constraints are enforced by the typing rules.) This stylized syntax makes the operational
semantics simple: a field access expression new C(e).f i just reduces to the corresponding constructor
argument e i . Also, since FJ does not have assignment statements, a method body always consists of a single
return statement: all the computation in the language goes on in the expressions following these returns.
A method invocation expression new C(e).m(d) is reduced by looking up the expression e 0 following the
return of method m in class C in the class table, and reducing to the instance of e 0 in which d and the
receiver object (new C(e)) are substituted for formal arguments and the special variable this, respectively.

Figure

4 states these reduction rules precisely.)
A program in FJ is a pair of a class table (a set of class definitions) and an expression (corresponding
to the main method in a Java program). The reduction relation is of the form e \Gamma! e
reduces to expression e
0 in one step." For example, given the class definitions
1 Of course, most useful examples of programming with inner classes do involve the side-effecting features of Java. However,
the core mechanisms of inner classes themselves do not interact with assignment in any interesting way. By omitting assignment
from FJ and FJI, we obtain a much simpler model that offers just as much insight into inner classes.
class Pair extends Object -
Object fst;
Object snd;
Pair(Object fst, Object snd) -
Pair setfst(Object newfst) -
return new Pair(newfst, this.snd);
class A extends Object -
class B extends Object -
the expression new Pair(new A(), new B()).setfst(new B()) reduces to new Pair(new B(), new B())
as follows
new Pair(new A(), new B()).setfst(new B())
\Gamma! new Pair(new B(), new Pair(new A(), new B()).snd)
\Gamma! new Pair(new B(), new B())
where the underlined subexpressions are the ones being reduced at each step.
3 FJ with Inner Classes
We now define the language FJI by extending FJ with inner classes. Like FJ, FJI imposes some syntactic
restrictions to simplify its operational semantics: (1) receivers of field access, method invocation, or inner class
constructor invocation must be explicitly specified (no implicit this); (2) type names are always absolute
paths to the classes they denote (no short abbreviations); and (3) an inner class instantiation expression
e.new C(e) is annotated with the static type T of e, written e.new!T? C(e).
Because of conditions (2) and (3), FJI is not quite a subset of Java (whereas FJ is); instead, we view
FJI as an intermediate language, to which the user's programs are translated by a process of elaboration.
We describe the elaboration process only informally here, since it is rather complex but not especially deep,
consisting mainly of a large number of rules for abbreviating long qualified names; a detailed treatment is
given in the companion technical report [5].
We begin with a brief discussion of the key idea of enclosing instances (Section 3.1). Then we discuss
the interactions between inner classes and subclassing (Section 3.2). Finally, we arrive at formal definitions
of the syntax (3.3) of FJI, some important auxiliary definitions (3.4), operational semantics (3.5), and the
typing relation (3.6). Statements of subject reduction and progress properties (3.7) finish the section.
3.1 Enclosing Instances
Consider the following FJI class declaration:
class Outer extends Object -
Pair
Outer(Pair p) -super();
class Inner extends Object -
Object snd-p - return Outer.this.p.snd; -
Outer.Inner make-inner () - return this.new!Outer? Inner(); -
Conceptually, each instance o of the class Outer contains a specialized version of the Inner class, which,
when instantiated, yields instances of Outer.Inner that refer to o's instance variable p. The object o is
called the enclosing instance of these Outer.Inner objects.
This enclosing instance can be named explicitly by a "qualified this" expression (found in both Java
and FJI), consisting of the simple name of the enclosing class followed by ".this". In general, the class
can refer to enclosing instances, C 1 .this to Cn\Gamma1 .this, as well as the usual this, which
can also be written Cn .this.
In FJI, an object of an inner class is instantiated by an expression of the form e.new!T? C(e), where e
is the enclosing instance and T is the static type of e. The result of e.new!T? C(e) is always an instance
of T.C, regardless of the run-time type of e. This rigidity reflects the static nature of Java's translation
semantics for inner classes. The explicit annotation !T? is used in FJI to "remember" the static type of e.
(By contrast, inner classes in Beta are virtual [7], i.e., different constructors may be invoked depending on
the run-time type of the enclosing instance; for example, if there were a subclass Outer 0 of the class Outer
that also had an inner class Inner, then o.new Inner() might build an instance of either Outer.Inner or
Outer 0 .Inner, depending on the dynamic type of o.)
The elaboration process allows type names to be abbreviated in Java programs. For example, the FJI
program above can be written
class Outer extends Object -
Pair
Outer(Pair p) -super();
class Inner extends Object -
Object snd-p () - return p.snd; -
Inner make-inner () - return new Inner(); -
in Java. Here, the return type Inner of the make-inner method denotes the nearest Inner declara-
tion. Also, in Java, enclosing instances can be omitted when they are this or a qualified this. Thus,
this.new!Outer? Inner() from the original example is written new Inner() here.
3.2 Subclassing and Inner Classes
Almost any form of inheritance involving inner classes is allowed in Java: a top-level class can extend an inner
class of another top-level class, or an inner class can extend another inner class from a completely different top-level
class. An inner class can even extend its own enclosing class. (Only one case is disallowed: a class cannot
extend its own inner class. We discuss the restriction later.) This liberality, however, introduces significant
complexity because a method inherited from a superclass must be executed in a "lexical environment"
different from subclass's. Figure 1 shows a situation where three inner classes, A1.A2.A3 and B1.B2.B3 and
C1.C2.C3, are in a subclass hierarchy. Each white oval represents an enclosing instance and the three shaded
ovals indicate the regions of the program where the methods of a C1.C2.C3 object may have been defined. A
method inherited from A1.A2.A3 is executed under the environment consisting of enclosing instances A1.this
and A2.this and may access members of enclosing classes via A1.this and A2.this; similarly B1.B2.B3
and C1.C2.C3. In general, when a class has n superclasses which are inner, n different environments may be
accessed by its methods. Moreover, each environment may consist of more than one enclosing instance; six
enclosing instances are required for all the methods of C1.C2.C3 to work in the example above.
From the foregoing, we see that we will have to provide, in some way, six enclosing instances to instantiate
a C1.C2.C3 object. Recall that, when an object of an inner class is instantiated, the enclosing object is
provided by a prefix e of the new expression. For example, a C1.C2.C3 object is instantiated by writing
e.new!C1.C2? C3(e), where e is the enclosing instance corresponding to C2.this. Where do the other
enclosing instances come from?
First, enclosing instances from enclosing classes other than the immediately enclosing class, such as
C1.this, do not have to be supplied to a new expression explicitly, because they can be reached via
extends
extends

Figure

1: A chain of environments
the direct enclosing instance-for example, the enclosing instance e in e.new!C1.C2? C3(e) has the form
new C1(c).new!C1? C2(d), which includes the enclosing instance new C1(c) that corresponds to C1.this.
Second, the enclosing instances of superclasses are determined by the constructor of a subclass. Taking
a simple example, suppose we extend the inner class Outer.Inner. An enclosing instance corresponding to
Outer.this is required to make an instance of the subclass. Here is an example of a subclass of Outer.Inner:
class RefinedInner extends Outer.Inner -
Object c;
RefinedInner(Outer this$Outer$Inner, Object c) -
In the declaration of the RefinedInner constructor, the ordinary argument this$Outer$Inner becomes the
enclosing instance prefix for the super constructor invocation, providing the value of Outer.this referred
to in the inherited method snd-p. Similarly, in the C1.C2.C3 example, the subclass B1.B2.B3 is written as
follows:
class B1 extends . -
class B2 extends . -
class B3 extends A1.A2.A3 -
Object b3;
B3(Object a3, A1.A2 this$A1$A2$A3, Object b3) -
Note that, since an enclosing instance corresponding to A1.this is included in an enclosing instance corresponding
to A2.this, the B3 constructor takes only one extra argument for enclosing instances. Here is
class:
class C1 extends . -
class C2 extends . -
class C3 extends B1.B2.B3 -
Object c3;
C3(Object a3, A1.A2 this$A1$A2$A3, Object b3, B1.B2 this$B1$B2$B3, Object c3) -
Since the constructor of a superclass B1.B2.B3 initializes A2.this, the constructor C3 initializes only B2.this
by qualifying the super invocation; the argument this$A1$A2$A3 is just passed to super as an ordinary
argument.
In FJI, we restrict the qualification of super to be a constructor argument, whereas Java allows any
expression for the qualification. This permits the same clean definition of operational semantics we saw in
FJ, since all the state information (including fields and enclosing instances) of an object appears in its new
expression. Moreover, for technical reasons connected with the name mangling involved in the translation
semantics, we require that a constructor argument used for qualification of super be named this$C 1
is the (direct) superclass, as in the example above.
Lastly, we can now explain why it is not allowed for a class to extend one of its (direct or indirect) inner
classes. It is because there is no sensible way to make an instance of such a class. Suppose we could define
the class below:
class Foo extends Foo.Bar -
class Bar -
Since Foo extends Foo.Bar, the constructor Foo will need an instance of Foo as an argument, making it
impossible to make an instance of Foo. (Perhaps one could use null as the enclosing instance in this case,
but this would not be useful, since inner classes are usually supposed to make use of enclosing instances.)
3.3 Syntax
Now, we proceed to the formal definitions of FJI. The abstract syntax of the language is shown at the top
left of Figure 2. We use the same notational conventions as in the previous section. The metavariables S, T,
and U ranges over types, which are qualified class names (a sequence of simple names C 1 ,. ,C n concatenated
by periods). For compactness in the definitions, we introduce the notation ? for a "null qualification" and
identify ?:C with C. The metavariable P ranges over types (T) and ? . We write
A class declaration L includes declarations of its simple name C, superclass T, fields T f, constructor K,
inner classes L, and methods M. There are two kinds of constructor declaration, depending on whether the
superclass is inner or top-level: when the superclass is inner, the subclass constructor must call the super
constructor with a qualification "f." to provide the enclosing instance visible from the superclass's methods.
As we will see in typing rules, constructor arguments should be arranged in the following order: (1) the
superclass's fields, initialized by super(f) (or f.super(f)); (2) the enclosing instance of the superclass (if
needed); and (3) the fields of the class to be defined, initialized by this.f=f. Like FJ, the body of a method
just returns an expression, which is a variable, field access, method invocation, or object instantiation. We
assume that the set of variables includes the special variables this and C.this for every C, and that these
variables are never used as the names of arguments to methods.
A program is a pair of a class table CT (a mapping from types T to class declarations L) and an expression
e. Object is treated specially in every FJI program: the definition of the Object class does not appear in
the class table and the auxiliary functions that look up fields and method declarations in the class table
are equipped with special cases for Object that return the empty sequence of fields and the empty set of
methods. To lighten the notation in what follows, we assume a fixed class table CT .
From the class table, we can read off the subtype relation between classes. We write
subtype of T-the reflexive and transitive closure of the immediate subclass relation given by the extends
clauses in CT . This relation is defined formally at the bottom left of Figure 2.
We impose the following sanity conditions on the class table: (1) CT class C . for every
has an inner class declaration L of name D, then CT
Object 62 dom(CT ). (4) For every type T (except Object) appearing anywhere in CT , we have T 2 dom(CT ).
(5) For every e 0 .new!T? C(e) (and new C(e), resp.) appearing anywhere in CT , we have T.C 2 dom(CT )
(and C 2 dom(CT ), resp. (6) There are no cycles in the subtyping relation. (7) T 6! : T.U, for any two types
T and T.U. By conditions (1) and (2), a class table of FJI can be identified with a set of top-level classes.
Condition (7) prohibits a class from extending one of its inner classes.
Syntax:
class C extends T -T f; K L M-
e ::= x
new C(e)
Computation:
new C(e).f i \Gamma! e i
cn
new C(e)
new C(e).m(d)
\Gamma!
ae
x 7! d; this 7! cn ;
i21:::n
oe
cn
\Gamma!
ae
x 7! d; this 7! cn ;
i21:::n
oe
Subtyping:
class C extends T -
Expression typing:
(IT-Field)
Method typing:
i21:::n
class Cn extends S -
if mtype(m;
(IT-Method)
Class typing:
M OK in P.C L OK in P.C
class C extends D -T f; K L M- OK IN P
M OK in P.C L OK in P.C
class C extends T.D -T f; K L M- OK IN P

Figure

2: FJI: Main Definitions
Field lookup:
class C extends D -T f; K L M-
class C extends U.D -T f; K L M-
class C extends S -S f; K L M-
class C extends S -S f; K L M-
m is not defined in M
Method body lookup:
class C extends S -S f; K L M-
class C extends S -S f; K L M-
m is not defined in M
Enclosing instance lookup:
encl T.C
class C extends D -S f; .-
encl T
(new C(d,
(new
class C extends U.D -S f; .-
encl T
(new C(d, d 0 , e))
class C extends D -S f; .-
encl T
(new
class C extends U.D -S f; .-
encl T

Figure

3: FJI: Auxiliary definitions
3.4 Auxiliary Functions
For the typing and reduction rules, we need a few auxiliary definitions, given in Figure 3. The fields of a
class T, written fields(T), is a sequence T f pairing the class of each field with its name, for all the fields
declared in class T and all of its superclasses. In addition, fields(T) collects the types of (direct) enclosing
instances of all the superclasses of T. For example, fields(C1.C2.C3) returns the following sequence:
Object a3, (the field from A1.A2.A3)
(enclosing instance bound A2.this)
Object b3, (the field from B1.B2.B3)
(enclosing instance bound to B2.this)
Object c3 (the field from C1.C2.C3)
The third rule in the definition inserts enclosing instance information between the fields S g of the superclass
U.D and the fields T f of the current class. In a well-typed program, fields(T) will always agree with the
constructor argument list of T.
The type of the method m in class T, written mtype(m; T), is a pair, written S!S, of a sequence of
argument types S and a result type S. Similarly, the body of the method m in class T, written mbody(m; T),
is a triple, written (x; e; T), of a sequence of parameters x, an expression e, and a class T where the method
is defined.
The function encl T
plays a crucial role in the semantics of FJI. Intuitively, when e is a top-level or
inner class instantiation, encl T
returns the direct enclosing instance of e that is visible from class T (i.e.,
the enclosing instance that provides the correct lexical environment for methods inherited from T). The
first rule is the simplest case: since the type of an expression e 0 .new!T? C(e) agrees with the subscript
T.C, it just returns the (direct) enclosing instance e 0 . The other rules follow a common pattern; we explain
the fifth rule as a representative. Since the subscripted type T is different from the type of the argument
the enclosing instance e 0 is not the correct answer. We therefore make a recursive
call with an object d 0 .new!U? D(d) of the superclass obtained by dropping e 0 and as many arguments e as
the fields f of the class S.C. We keep going like this until, finally, the argument becomes an instance of T
and we match the first rule. For example:
encl A1.A2.A3
(e.new!C1.C2? C3(a, new A1().new!A1? A2(), b, new B1().new!B1? B2(), c))
(new B1().new!B1? B2.new!B1.B2? B3(a, new A1().new!A1? A2(), b))
(new A1().new!A1? A2().new!A1.A2? A3(a))
new A1().new!A1? A2()
Note that the encl function outputs only the direct enclosing instance. To obtain outer enclosing instances,
such as A1.this, encl can be used repeatedly: encl A1.A2
(encl A1.A2.A3
(e)).
Computation
As in FJ, the reduction relation of FJI has the form e \Gamma! e 0 . We write \Gamma!   for the reflexive and transitive
closure of \Gamma!. The reduction rules are given in the middle of the left column of Figure 2. There are four
reduction rules, two for field access and two for method invocation. The field access expression new C(e).f i
looks up the field names f of C using fields(C) and yields the constructor argument e i in the position
corresponding to f i in the field list; e.new!T? C(e).f i behaves similarly. The method invocation expression
new C(e).m(d) first calls mbody(m; C) to obtain a triple of the sequence of formal arguments x, the method
body e, and the class C 1 . \Delta \Delta \Delta .Cn where m is defined; it yields a substitution instance of the method body
in which the x are replaced with the actual arguments d, the special variables this and Cn.this with
the receiver object new C(e), and each C i .this (for n) with the corresponding enclosing instance c i ,
obtained from encl . Since the method to be invoked is defined in C 1 . \Delta \Delta \Delta .Cn , the direct enclosing instance
.this is obtained by encl C 1 .\Delta\Delta\Delta.C n
(e), where e is the receiver object; similarly, Cn\Gamma2 .this is obtained by
encl C1 .\Delta\Delta\Delta.C
(encl C1 .\Delta\Delta\Delta.C n
(e)), and so on. The reduction rules may be applied at any point in an expression,
so we also need the obvious congruence rules (if e \Gamma! e
.f, and the like), which we omit
here.
For example, if the class table includes Outer, RefinedInner, Pair, A, and B, then
new RefinedInner(new Outer(new Pair(new A(), new B())), new Object()).snd-p()
reduces to new B() as follows,
new RefinedInner(new Outer(new Pair(new A(), new B())), new Object()).snd-p()
\Gamma! new Outer(new Pair(new A(), new B())).p.snd
\Gamma! new Pair(new A(), new B()).snd
\Gamma! new B()
where the underlined subexpressions are the redices at each reduction step.
3.6 Typing Rules
The typing rules for expressions, method declarations, and class declarations are given in the right-hand
column of Figure 2.
An environment \Gamma is a finite mapping from variables to types, written x:T. The typing judgment for
expressions has the form \Gamma ' e 2 T, read "in the environment \Gamma, expression e has type T." The typing rules
are syntax directed, with one rule for each form of expression. The typing rules for object instantiations and
method invocations check that each actual parameter has a type which is a subtype of the corresponding
formal parameter type obtained by fields or mtype; the enclosing object must have a type which is a subtype
of the annotated type T in new !T?.
The typing judgment for method declarations has the form M OK IN C 1 . \Delta \Delta \Delta .Cn , read "method declaration
M is ok if it is declared in class C 1 . \Delta \Delta \Delta .Cn ." The body of the method is typed under the context in which
the formal parameters of the method have their declared types and each C i .this has the type C 1 . \Delta \Delta \Delta .C i . If
a method with the same name is declared in the superclass then it must have the same type in the subclass.
The typing judgment for class declarations has the form L OK IN P, read "class declaration L is ok if it
is declared in P." If P is a type T, the class declaration L is an inner class; otherwise, L is a top-level class.
The typing rules check that the constructor applies super to the fields of the superclass and initializes the
fields declared in this class, and that each method declaration and inner class declaration in the class is ok.
The condition C 62 P ensures that the (simple) class name to be defined is not also a simple name of one of
the enclosing classes, so as to avoid ambiguity of the meaning of C.this.
3.7 Properties
It is easy to show that FJI programs enjoy standard subject reduction and progress properties, which together
guarantee that well-typed programs never cause NoSuchFieldError or NoSuchMethodError.
3.7.1 Theorem [Subject Reduction]: If \Gamma ' e 2 T and e \Gamma! e
0 such that
Proof sketch: The main property required in the proof is the following term-substitution lemma:
If
This is proved by induction on the derivation of \Gamma; plus the following lemma:
such that
Similarly for e 0
The theorem itself is now proved by induction on the derivation of e \Gamma! e 0 , with a case analysis on the last
rule used. The cases for IR-InvkT and IR-InvkI are easy using the lemmas above. The other base cases
are also straightforward, as are the induction steps. \Xi
3.7.2 Theorem [Progress]: Suppose e is a well-typed expression.
(1) If e includes new C 0 (e).f as a subexpression, then fields(C 0 Similarly, if e includes
(2) If e includes new C 0 (e).m(d) as a subexpression, then mbody(m; C
Similarly, if e includes e 0
and
Translation Semantics
In this section we consider the other style of semantics: translation from FJI to FJ. Every inner class
is compiled to a top-level class with one additional field holding a reference to the direct enclosing in-
stance; occurrences of qualified this are translated into accesses to this field. For example, the Outer and
RefinedInner classes in the previous section are compiled to the following three FJ classes.
class Outer extends Object -
Pair
Outer$Inner make-inner () - return new Outer$Inner(this); -
class Outer$Inner extends Object -
Outer
Outer$Inner(Outer this$Outer$Inner) -
Object snd-p - return this.this$Outer$Inner.p.snd; -
class RefinedInner extends Outer$Inner -
Object c;
RefinedInner(Outer this$Outer$Inner, Object c) -
The inner class Outer.Inner is compiled to the top-level class Outer$Inner; the field this$Outer$Inner
holds an Outer object, which corresponds to the direct enclosing instance Outer.this in the original FJI
program; thus, Outer.this is compiled to the field access expression this.this$Outer$Inner.
We give a compilation function j \Delta j for each syntactic category. Except for types, the compilation functions
take as their second argument the FJI class name (or, ?) where the entity being translated is defined, written
(or
4.1 Types, Expressions and Methods
Every qualified class name is translated to a simple name obtained by syntactic replacement of . with $.
The compilation of expressions, written jej T
, is given below. We write jej T
as shorthand for je
(and similarly for
and
jnew D(e)j T
new D( jej T
new jT.Dj ( jej T
As we saw above, a compiled inner class has one additional field, called this$ jTj, where T is the original
class name. C i .this in the class C 1 . \Delta \Delta \Delta .Cn becomes an expression that follows references to the direct
enclosing instance in sequence until it reaches the correct one. An enclosing instance e 0 of e 0 .new!T? C(e)
will become the last argument of the compiled constructor invocation.
Compilation of methods, written jMj T
, is straightforward.
stands for jT 1
4.2 Constructors and Classes
Compilation of constructors, written jKj T
, is given below.
It has four cases, depending on whether the current class is a top-level class or an inner class and whether its
superclass is a top-level class or an inner class. When the current class is an inner class, one more argument
corresponding to the enclosing instance is added to the argument list; the name of the constructor becomes
jT.Cj, the translation of the qualified name of the class. When the superclass is inner, the argument used for
the qualification of f.super(f) becomes the last argument of the super() invocation.
Finally, the compilation of classes, written jLj P
, is as follows:
class C extends S -T f; K L M-
class C extends jSj -
class C extends S -T f; K L M-
class jT.Cj extends jSj -
The constructor, inner classes, and methods of class C defined in P are compiled with auxiliary argument P.C.
Inner classes L become top-level classes. As in constructor compilation, when the compiled class is inner, its
name changes to jT.Cj and the field this$ jT.Cj, holding an enclosing instance, is added. The compilation
of the class table, written jCT j, is achieved by compiling all top-level classes L in CT (i.e.,
4.3 Properties of Translation Semantics
It is easy to show that the translation semantics preserves typing, in the sense that a well-typed FJI program
is compiled to a well-typed FJ program.
4.3.1 Theorem [Compilation preserves typing]: If CT is ok and with respect to CT ,
with respect to jCT j and jCT j is ok.
Finally, we come to the main result of this section: the correspondence of the direct semantics presented in
the previous section and the translation semantics defined here. We show that the behavior of a compiled
program exactly reflects the behavior of the original program in FJI: for every step of reduction of an
well-typed FJI program, the compiled program takes one or more steps and reaches a corresponding state.
4.3.2 Theorem [Compilation commutes with reduction]: If \Gamma ' FJI e 2 T and e\Gamma! FJI e
\Gamma! FJ
Proof straightforward induction on the derivation of e \Gamma! FJI e
0 with a case analysis on the
last rule used. The main lemma for the cases IR-InvkT and IR-InvkI is:
Suppose 2. If
we have jnew C(e)j ?
(new C(e))j ?
Similarly, if
This lemma shows that the calculation of encl T
(e) is correctly mimicked by field access to the mangled fields
in the translation. Since method invocation in the direct semantics may involve calculation
of encl (\Delta \Delta \Delta) several times, the low-level reduction may require more than one step to mimic one step at the
FJI level. \Xi
5 Conclusions and Future Work
We have formalized two styles of semantics for inner classes: a direct style and a translation style, where
semantics is given by compilation to a low-level language without inner classes, following Java's Inner Classes
Specification. We have proved that the two styles correspond, in the sense that the translation commutes
with the high-level reduction relation in the direct semantics. Besides deepening our own understanding of
inner classes, this work has uncovered several bugs in various Java compilers.
For future work, the interaction between inner classes and access restrictions in Java is clearly worth
investigating. We also hope to be able to model Java's other forms of inner classes: anonymous classes and
local classes, which can be declared in method bodies; these are slightly more complicated, since method
arguments (not just fields) can occur in them as free variables, but we expect they can be captured by a
variant of FJI.

Acknowledgments

This work was supported by the University of Pennsylvania and the National Science Foundation under grant
CCR-9701826, Principled Foundations for Programming with Objects. Igarashi is a research fellow of the
Japan Society of the Promotion of Science. We would like to thank bug parade in Java Developer Connection
(http://developer.java.sun.com/developer/bugParade/index.html) for providing useful information.



--R

A secure implementation of java inner classes.
Making the future safe for the past: Adding genericity to the Java programming language.

Featherweight Java: A minimal core calculus for Java and GJ.
On inner classes.


Birger M-ller-Pedersen
--TR
Smalltalk-80: the language and its implementation
Virtual classes: a powerful mechanism in object-oriented programming
Java<i><sub>light</sub></i> is type-safeMYAMPERSANDmdash;definitely
Classes and mixins
Making the future safe for the past
Is the Java type system sound?
Semantic analysis of virtual classes and tested classes
Featherwieght Java
The C++ Programming Language, Third Edition
The Java Language Specification
A Statically Safe Alternative to Virtual Types
Protection in Programming-Language Translations

--CTR
Nathaniel Nystrom , Stephen Chong , Andrew C. Myers, Scalable extensibility via nested inheritance, ACM SIGPLAN Notices, v.39 n.10, October 2004
D. Ancona , C. Anderson , F. Damiani , S. Drossopoulou , P. Giannini , E. Zucca, A provenly correct translation of Fickle into Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.2, p.13-es, April 2007
Christopher League , Zhong Shao , Valery Trifonov, Type-preserving compilation of Featherweight Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.2, p.112-152, March 2002
Radha Jagadeesan , Alan Jeffrey , James Riely, Typed parametric polymorphism for aspects, Science of Computer Programming, v.63 n.3, p.267-296, 15 December 2006
language design;inner classes;language semantics