19.2 Overview

< Free Open Study >

In FJ, a program consists of a collection of class definitions plus a term to be evaluated, corresponding to the body of the main method in full Java. Here are some typical class definitions in FJ.

   class A extends Object { A() { super(); } }   class B extends Object { B() { super(); } }   class Pair extends Object {     Object fst;     Object snd;     // Constructor:     Pair(Object fst, Object snd) {       super(); this.fst=fst; this.snd=snd; }     // Method definition:     Pair setfst(Object newfst) {       return new Pair(newfst, this.snd); } }

For the sake of syntactic regularity, we always include the superclass (even when it is Object), we always write out the constructor (even for the trivial classes A and B), and we always name the receiver in a field access or a method invocation (as in this.snd), even when the receiver is this. Constructors always take the same stylized form: there is one parameter for each field, with the same name as the field; the super constructor is invoked to initialize the fields of the superclass; and then the remaining fields are initialized to the corresponding parameters. In this example, the superclass of all three classes is Object, which has no fields, so the invocations of super have no arguments. Constructors are the only place where super or = appears in an FJ program. Since FJ provides no side-effecting operations, a method body always consists of return followed by a term, as in the body of setfst().

There are five forms of term in FJ. In the example, new A(), new B(), and new Pair(...,...) are object constructors, and ... .setfst(...) is a method invocation. In the body of setfst, the term this.snd is a field access, and the occurrences of newfst and this are variables.^[2] In the context of the above definitions, the term

   new Pair(new A(), new B()).setfst(new B())

evaluates to new Pair(new B(), new B()).

The remaining form of term is a cast (see §15.5). The term

   ((Pair)new Pair(new Pair(new A(), new B()),                   new A()).fst).snd

evaluates to new B(). The subterm (Pair)t, where t is new Pair(...).fst, is a cast. The cast is required, because t is a field access to fst, which is declared to contain an Object, whereas the next field access, to snd, is valid only on a Pair. At run time, the evaluation rules check whether the Object stored in the fst field is a Pair (in this case the check succeeds).

Dropping side effects has a pleasant side effect: evaluation can easily be formalized entirely within the syntax of FJ, with no additional mechanisms for modeling the heap (see Chapter 13). There are three basic computation rules: one for field access, one for method invocation, and one for casts. Recall that, in the lambda-calculus, the evaluation rule for applications assumes that the function is first simplified to a lambda abstraction. Similarly, in FJ the evaluation rules assume the object operated upon is first simplified to a new term. The slogan in the lambda-calculus is "everything is a function"; here, "everything is an object."

The next example shows the rule for field access (E-PROJNEW) in action:

   new Pair(new A(), new B()).snd →  new()

Because of the stylized syntax of object constructors, we know that the constructor has one parameter for each field, in the same order that the fields are declared. Here the fields are fst and snd, and an access to the snd field selects the second parameter.

Here is the rule for method invocation (E-INVKNEW) in action:

The receiver of the invocation is the object new Pair(new A(),new B()), so we look up the setfst method in the Pair class, where we find that it has formal parameter newfst and body new Pair(newfst, this.snd). The invocation reduces to the body with the formal parameter replaced by the actual, and the special variable this replaced by the receiver object. This is similar to the beta-reduction rule (E-APPABS) of the lambda-calculus. The key differences are the fact that the class of the receiver determines where to look for the body (supporting method override), and the substitution of the receiver for this (supporting "open recursion through self").^[3] In FJ, as in the lambda-calculus, if the formal parameter appears more than once in the body this may lead to duplication of the argument value, but since there are no side effects this difference from the standard Java semantics cannot be observed.

Here is the rule for casts (E-CASTNEW) in action:

   (Pair)new Pair(new A(), new B()) →  new Pair(new A(), new B())

Once the subject of the cast is reduced to an object, it is easy to check that the class of the constructor is a subclass of the target of the cast. If so (as is the case here), the reduction removes the cast. If not, as in the term (A)new B(), then no rule applies and the computation is stuck, denoting a run-time error.

There are three ways in which a computation may get stuck: an attempt to access a field not declared for the class, an attempt to invoke a method not declared for the class ("message not understood"), or an attempt to cast to something other than a superclass of an object's run-time class. We will prove that the first two of these never happen in well-typed programs, and that the third never happens in well-typed programs that contain no downcasts (and no "stupid casts"—a technicality explained below).

We adopt a standard call-by-value evaluation strategy. Here are the steps of evaluation for the second example term above, where the next subterm to be reduced is underlined at each step.

^[2]The syntax of FJ differs slightly from Java in treating this as a variable, not a keyword.

^[3]Readers familiar with Abadi and Cardelli's object calculus (1996) will see a strong similarity to their ζ-reduction rule.

< Free Open Study >