|< Free Open Study >|
The syntax of FJ is given in Figure 19-1. The metavariables
A, B, C, D
range over class
Figure 19-1: Featherweight Java (Syntax and Subtyping)
We write as shorthand for f 1 ,..., f n (similarly , , , etc.) and write for M 1 ... M n (with no commas). We abbreviate operations on pairs of sequences similarly, writing " " for " C 1 f 1 ,..., C n f n ", where n is the length of and , ;" for the declarations " C 1 f 1 ;... C n f n ;" and " " for " this.f 1 = f 1 ;...; this.f n = f n ;". Sequences of field declarations, parameter names, and method declarations are assumed to contain no duplicate names.
introduces a class named
. The new class has fields
, a single constructor
, and a suite of
The constructor declaration shows how to initialize the fields of an instance of C . Its form is completely determined by the instance variable declarations of C and its superclasses: it must take exactly as many parameters as there are instance variables, and its body must consist of a call to the superclass constructor to initialize its fields from the parameters , followed by an assignment of the parameters to the new fields of the same names declared by C . (These constraints are enforced by the typing rule for classes in Figure 19-4.) In full Java, a subclass constructor must contain a call to its superclass constructor (when the superclass constructor takes arguments); this is the reason that the constructor body here calls super to initialize the superclass's instance variables. If we did not care about making FJ a literal subset of Java, we could drop the call to super and make each constructor initialize all the instance variables directly.
The method declaration introduces a method named m with result type D and parameters of types . The body of the method is the single statement return t . The variables are bound in t . The special variable this is also considered bound in t .
A class table
is a mapping from class names
to class declarations
. A program is a pair (
) of a class table and a
Every class has a superclass, declared with extends . This raises a question: what is the superclass of the Object class? There are various ways to deal with this issue; the simplest one (which we adopt here) is to take Object as a distinguished class name whose definition does not appear in the class table. The auxiliary function that looks up fields in the class table is equipped with a special case for Object that returns the empty sequence of fields, denoted ; Object is also assumed to have no methods. 
By looking at the class table, we can read off the subtype relation between classes. We write
C <: D
is a subtype of
i.e., subtyping is the reflexive and transitive closure of the immediate subclass relation given by the
. It is defined
The given class table is assumed to
Note that the types defined by the class table are allowed to be recursive, in the sense that the definition of a class A may use the name A in the types of its methods and instance variables. Mutual recursion between class definitions is also allowed.
By analogy with the S-TOP rule in our lambda-calculus with subtyping, one might expect to see a rule
For the typing and evaluation rules, we will need a few auxiliary definitions; these are given in Figure 19-2. The fields of a class
), is a sequence
Figure 19-2: Featherweight Java (Auxiliary Definitions)
We use a standard call-
Figure 19-3: Featherweight Java (Evaluation)
Note that the run-time behavior of the cast operation is to test whether the actual type of the object being cast is a subtype of the type declared in the cast. If it is, then the cast operation is thrown away and the result is the object itself. This corresponds exactly to the semantics of Java: a run-time cast does not change an object in any way it simply either succeeds or else fails and raises an exception. In FJ, instead of raising an exception a failing cast will just get stuck, since there will be no evaluation rule that applies.
The typing rules for terms, method declarations, and class declarations are given in Figure 19-4. An environment is a finite mapping from variables to types, written . Typing statements for terms have the form ⊢ t : C , read "in the environment , term t has type C ." The typing rules are syntax directed,  with one rule for each form of term, save that there are three rules for casts (discussed below). The typing rules for constructors and method invocations check that each argument has a type that is a subtype of the one declared for the corresponding formal parameter. We abbreviate typing statements on sequences in the obvious way, writing as shorthand for ⊢ t 1 : C 1 ,..., ⊢ t n : C n and as shorthand for C 1 <: D 1 ,..., C n <: D n .
Figure 19-4: Featherweight Java (Typing)
One minor technical innovation in FJ is the introduction of "stupid" casts. There are three rules for type casts: in an
the subject is a subclass of the target, in a
Typing statements for method declarations have the form
M OK in C
, read "method declaration
Typing statements for class declarations have the form CL OK , read "class declaration CL is well formed." It checks that the constructor applies super to the fields of the superclass and initializes the fields declared in this class, and that each method declaration in the class is ok.
The type of a term may depend on the type of any methods it invokes, and the type of a method depends on the type of a term (its body), so it behooves us to check that there is no ill-defined circularity here. Indeed there is none: the circle is broken because the type of each method is explicitly declared. It is possible to load the class table and use it for
A number of design decisions in FJ are dictated by the
The operation of assigning a new value to the field of an object is omitted from FJ to simplify its presentation, but it can be added without changing the basic character of the calculus very much. Do this, using the treatment of references in Chapter 13 as a model.
Extend FJ with analogs of Java's raise and try forms, using the treatment of exceptions in Chapter 14 as a model.
FJ, like full Java,
Full Java provides both classes and
, which specify the types of methods, but not their
The presence of interfaces in Java actually forces the choice of an algorithmic presentation of the typing relation, which gives each typable term a unique (minimal) type. The reason is an interaction between conditional expressions (written t 1 ? t 2 : t 3 in Java) and interfaces.
Show how to extend FJ with interfaces in the style of Java.
Show that, in the presence of interfaces, the subtype relation is not
What is Java's typing rule for conditional expressions? Is it reasonable?
FJ includes Java's this keyword, but omits super . Show how to add it.
In Java, instance variables of superclasses may be redeclared
 In full Java, the class Object actually has several methods. We ignore these in FJ.
 We follow full Java in choosing an algorithmic formulation of the typing relation. Interestingly, in full Java this choice is actually forced. See Exercise 19.4.6.
|< Free Open Study >|