Featherweight Java

Featherweight Java (FJ) is a minimal core calculus for Java as defined in Featherweight Java: A Minimal Core Calculus for Java and GJ, Atsushi Igarashi and Benjamin C. Pierce, ACM Transactions on Programming Languages and Systems, Vol. 23, No. 3, May 2001, Pages 396-450. An implementation of an Interpreter for the dynamic semantics of FJ is available at: trunk/ProjectFortress/demos/FeatherweightJava.fss.

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 Java.) The abstract syntax of FJ class declarations, constructor declarations, method declarations, and expressions is given as follows in the paper:

and is implemented in Fortress as follows:

Loading...

Subtyping rules and field, method type, and method body lookup are defined within the object ClassTable:

Loading...

Subtyping is the reflexive and transitive closure of the immediate subclass relation given by the 'extends' clauses in a class table CT. Formally, it is defined as follows:

implemented as follows:

Loading...

and invoked under a given class table (in a rendered form) :

For the typing and reduction rules, a few auxiliary lookup definitions are given. Field lookup is formally defined as follows:

and implemented as follows:

Loading...

and method type and body lookups are formally defined as follows:

and implemented as follows:

Loading...

The following dynamic semantics of FJ:

is implemented as methods of objects extending the trait Expr:

Loading...

For example, the evaluation of a method invocation is implemented as follows (in a rendered form) :

and invoked under a given class table and an environment (in a rendered form) :

After implementing FJ as described in the paper, trunk/ProjectFortress/demos/FeatherweightJava.fss runs some tests using a class table CT including the following class:

Loading...

For example, the following tests:

assert that under the given pair of a class table and an environment, the left-hand side of -> is evaluated to the right-hand side of ->.