19.4 Definitions

< Free Open Study >

We now turn to the formal definition of FJ.

Syntax

The syntax of FJ is given in Figure 19-1. 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; s and t range over terms; u and v range over values; CL ranges over class declarations; K ranges over constructor declarations; M ranges over method declarations. We assume that the set of variables includes the special variable this, but that this is never used as the name of an argument to a method. Instead, it is considered to be implicitly bound in every method declaration. The evaluation rule for method invocation (rule E-INVKNEW in Figure 19-3) will substitute an appropriate object for this in addition to substituting argument values for parameters.

Figure 19-1: Featherweight Java (Syntax and Subtyping)

We write as shorthand for f₁,...,f_n (similarly , , , etc.) and write for M₁...M_n (with no commas). We abbreviate operations on pairs of sequences similarly, writing "" for "C₁ f₁,...,C_n f_n", where n is the length of and , ;" for the declarations "C₁ f₁;...C_n f_n;" and "" for "this.f₁=f₁;...; this.f_n=f_n;". Sequences of field declarations, parameter names, and method declarations are assumed to contain no duplicate names.

The declaration introduces a class named C with superclass D. The new class has fields with types , a single constructor K, and a suite of methods . The instance variables declared by C are added to the ones declared by D and its superclasses, and should have names distinct from these.^[4] The methods of C, on the other hand, may either override methods with the same names that are already present in D or add new functionality special to C.

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 CT is a mapping from class names C to class declarations CL. A program is a pair (CT, t) of a class table and a term. To lighten the notation in what follows, we always assume a fixed class table CT.

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.^[5]

By looking at the class table, we can read off the subtype relation between classes. We write C <: D when C is a subtype of D—i.e., subtyping is the reflexive and transitive closure of the immediate subclass relation given by the extends clauses in CT. It is defined formally in Figure 19-1.

The given class table is assumed to satisfy some sanity conditions: (1) CT(C) = class C... for every C Î dom(CT); (2) Object ∉ dom(CT); (3) for every class name C (except Object) appearing anywhere in CT, we have C Î dom(CT); and (4) there are no cycles in the subtype relation induced by CT—that is, the <: relation is antisymmetric.

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.

19.4.1 Exercise [⋆]

By analogy with the S-TOP rule in our lambda-calculus with subtyping, one might expect to see a rule stating that Object is a supertype of every class. Why don't we need it here?

Auxiliary Definitions

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 C, written fields(C), is a sequence pairing the class of each field with its name, for all the fields declared in class C and all of its superclasses. The type of the method m in class C, written mtype(m, C), is a pair, written , of a sequence of argument types and a single result type B. Similarly, the body of the method m in class C, written mbody(m, C), is a pair, written , of a sequence of parameters and a term t. The predicate override(m, D, ) judges whether a method m with argument types and a result type C₀ may be defined in a subclass of D. In case of overriding, if a method with the same name is declared in the superclass then it must have the same type.

Figure 19-2: Featherweight Java (Auxiliary Definitions)

Evaluation

We use a standard call-by-value operational semantics (Figure 19-3). The three computation rules—for field access, method invocation, and casting—were explained in §19.2. The rest of the rules formalize the call-by-value strategy. The values that can result from normal termination of the evaluator are fully evaluated object creation terms of the form .

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.

Typing

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,^[6] 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₁ : C₁,..., Г ⊢ t_n : C_n and as shorthand for C₁ <: D₁,..., 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 upcast the subject is a subclass of the target, in a downcast the target is a subclass of the subject, and in a stupid cast the target is unrelated to the subject. The Java compiler rejects as ill typed a term containing a stupid cast, but we must allow stupid casts in FJ if we are to formulate type safety as a type preservation theorem for a small-step semantics. This is because a sensible term may be reduced to one containing a stupid cast. For example, consider the following, which uses classes A and B as defined in §19.2:

We indicate the special nature of stupid casts by including the hypothesis stupid warning in the type rule for stupid casts (T-SCAST); an FJ typing corresponds to a legal Java typing only if it does not contain this rule.

Typing statements for method declarations have the form M OK in C, read "method declaration M is well formed if it occurs in class C." It uses the term typing relation on the body of the method, where the free variables are the parameters of the method with their declared types, plus the special variable this with type C.

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 typechecking before all the classes in it have been checked, so long as each class is eventually checked.

19.4.2 Exercise [⋆⋆]

A number of design decisions in FJ are dictated by the desire to make it a subset of Java, in the sense that every well- or ill-typed FJ program is well- or ill-typed as a Java program, and the well-typed programs behave the same. Suppose this requirement were dropped—i.e., suppose all we wanted was a Java-like core calculus. How would you change the design of FJ to make it simpler or more elegant?

19.4.3 Exercise [Recommended, ⋆⋆⋆ ↛]

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.

19.4.4 Exercise [⋆⋆⋆ ↛]

Extend FJ with analogs of Java's raise and try forms, using the treatment of exceptions in Chapter 14 as a model.

19.4.5 Exercise [⋆⋆ ↛]

FJ, like full Java, presents the typing relation in algorithmic form. There is no subsumption rule; instead, several of the other rules include subtyping checks among their premises. Can the system be reformulated in a more declarative style, dropping most or all of these premises in favor of a single subsumption rule?

19.4.6 Exercise [⋆⋆⋆]

Full Java provides both classes and interfaces, which specify the types of methods, but not their implementations. Interfaces are useful because they permit a richer, non-tree-structured, subtype relation: each class has a single superclass (from which it inherits instance variables and method bodies), but may additionally implement any number of interfaces.

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₁ ? t₂ : t₃ 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 necessarily closed under joins. (Recall from §16.3 that the existence of joins played a critical role in the minimal typing property for conditionals.)
What is Java's typing rule for conditional expressions? Is it reasonable?

19.4.7 Exercise [⋆⋆⋆]

FJ includes Java's this keyword, but omits super. Show how to add it.

^[4]In Java, instance variables of superclasses may be redeclared—the redeclaration shadows the original in the current class and its subclasses. We omit this feature in FJ.

^[5]In full Java, the class Object actually has several methods. We ignore these in FJ.

^[6]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 >