26-11-2012, 10:48 AM
Featherweight Java: A Minimal Core Calculus for Java and GJ
1Featherweight Java.pdf (Size: 629.28 KB / Downloads: 19)
ABSTRACT
Several recent studies have introduced lightweight versions of Java: reduced languages in which
complex features like threads and reflection are dropped to enable rigorous arguments about
key properties such as type safety. We carry this process a step further, omitting almost all features
of the full language (including interfaces and even assignment) to obtain a small calculus,
Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight
Java bears a similar relation to Java as the lambda-calculus does to languages such as ML
and Haskell. It offers a similar computational “feel,” providing classes, methods, fields, inheritance,
and dynamic typecasts with a semantics closely following Java’s. A proof of type safety for
Featherweight Java thus illustrates many of the interesting features of a safety proof for the full
language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational
semantics of Featherweight Java make it a handy tool for studying the consequences of extensions
and variations. As an illustration of its utility in this regard, we extend Featherweight Java with
generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed
proof of type safety. The extended system formalizes for the first time some of the key features
of GJ.
INTRODUCTION
Formal modeling can offer a significant boost to the design of complex real-world
artifacts such as programming languages. A formal model may be used to describe
some aspect of a design precisely, to state and prove its properties, and
to direct attention to issues that might otherwise be overlooked. In formulating
a model, however, there is a tension between completeness and compactness:
The more aspects the model addresses at the same time, the more unwieldy
it becomes. Often it is sensible to choose a model that is less complete but
more compact, offering maximum insight for minimum investment. This strategy
may be seen in a flurry of recent papers on the formal properties of Java,
which omit advanced features such as concurrency and reflection and concentrate
on fragments of the full language to which well-understood theory can
be applied.
We propose Featherweight Java, or FJ, as a new contender for a minimal core
calculus for modeling Java’s type system. The design of FJ favors compactness
over completeness almost obsessively, having just five forms of expression: object
creation, method invocation, field access, casting, and variables. Its syntax,
typing rules, and operational semantics fit comfortably on a few pages. Indeed,
our aim has been to omit as many features as possible—even assignment—
while retaining the core features of Java typing. There is a direct correspondence
between FJ and a purely functional core of Java, in the sense that every
FJ program is literally an executable Java program.
FEATHERWEIGHT JAVA
In FJ, a program consists of a collection of class definitions plus an expression
to be evaluated. (This expression corresponds to the body of the main method
in full Java.) Here are some typical class definitions in FJ.
Typing
The typing rules for expressions, method declarations, and class declarations
are in Figure 2. An environment 0 is a finite mapping from variables to types,
written ¯x:¯C. The typing judgment for expressions has the form 0 ` e : C, read
“in the environment 0, expression e has type C.” We abbreviate typing judgments
on sequences in the obvious way, writing 0 ` ¯e : ¯Cas shorthand for 0 `
e1 : C1, : : : , 0 ` en : Cn and writing ¯C<:¯Das shorthand for C1 <: D 1, : : : , Cn <n.
The typing rules are syntax directed, with one rule for each form of expression,
save that there are three rules for casts. Most of them are straightforward
adaptations of the rules in Java; the typing rules for constructors and method
invocations check that each actual parameter has a type that is a subtype of
the corresponding formal parameter type.
Reduction
The reduction relation is of the form e!e0, read “expression e reduces
to expression e0 in one step.” We write! for the reflexive and transitive
closure of!.
The reduction rules are given in Figure 3. There are three reduction rules,
one for field access, one for method invocation, and one for casting. These were
already explained in the introduction to this section. We write [¯d=¯x, e=y]e0 for
the result of replacing x1 by d1, : : : , xn by dn, and y by e in expression e0.
The reduction rules may be applied at any point in an expression, so we
also need the obvious congruence rules (if e!e0 then e.f!e0.f, and the like),
which also appear in the figure.2
Properties
Formal definitions are fun, but the proof of the pudding is in : : : well, the proof. If
our definitions are sensible, we should be able to prove a type soundness result,
which relates typing to computation. Indeed, we can prove such a result: if a
term is well typed and it reduces to a normal form, then it is either a value
of a subtype of the original term’s type, or an expression that gets stuck at a
downcast. The type-soundness theorem (Theorem 2.4.3) is proved by using the
standard technique of subject reduction and progress theorems [Wright and
Felleisen 1994].
Reduction
The operational semantics of FGJ programs is only a little more complicated
than what we had in FJ. The rules appear in Figure 8. In the
rule GR-CAST, the empty environment ; indicates the fact that whether or
not N is a subtype of P must be checked without information on runtime
type arguments.
Properties
Type Soundness. FGJ programs enjoy subject reduction, progress properties,
and thus a type soundness property exactly like programs in FJ
(Theorems 3.4.1, 3.4.2, and 3.4.3), The basic structures of the proofs are similar
to those of Theorems 2.4.1 and 2.4.2. For subject reduction, however, since
we now have parametric polymorphism combined with subtyping, we need a
few more lemmas The main lemmas required are a term substitution lemma
as before, plus similar lemmas about the preservation of subtyping and typing
under type substitution. (Readers familiar with proofs of subject reduction
for typed lambda-calculi like F [Cardelli et al. 1994] will notice many similarities).
The required lemmas include three substitution lemmas, which are
proved by straightforward induction on a derivation of 1 ` S<:T or 1; 0 ` e:T.
In the following proof, the underlying class table is assumed to be ok.