# Transition rules for Java - JVM

« Previous Topics
Static Semantics Of Java

Transition rules describe how the states of JavaI, i.e., the dynamic functions restbody; pos; locals, change over time by evaluating expressions and executing statements of the input program. Initially restbody is the given method body, pos is its start position _rstPos and locals is empty. The machine execJavaI , depending on its currently to be executed subterm, either evaluates an expression, or executes a statement. This work is done by two submachines execJavaExpI and execJavaStmI which are de_ned below, so that execJavaI is the following machine:

The machine execJavaI terminates if none of the rules of its submachines can be applied any more. Before proceeding in the next subsections to the de_nition of these two submachines, we explain here the basic mechanism they share, also with the other machines to be de_ned in this chapter, for walking through the abstract syntax tree.

When the machine encounters a stm to be executed or an exp to be evaluated, or when it comes (back) to the _rstPos of its method body, the context of the pending subcomputation of this phrase is given by restbody=pos. After this subcomputation has been completed, either normally or abruptly, the control passes to the parent position where the decision is taken on how to continue, either by computing the next subphrase of the phrase in the parent position, or by executing on the computed subphrases the computation to be done at the parent position. In both cases the context of the completed subcomputation changes to the superphrase restbody = up(pos); here the auxiliary function up: Pos ! Pos yields the parent position of a position, thus allowing to retrieve for a phrase, occurring in a position, the next enclosing phrase. We capture this context switch by the following de_nition.

Since the context switch is often accompanied by passing to the parent position the result of the completed subcomputations, or what has to be computed from them at the parent position, we use the following rule:

It combines passing a result, from a substructure at pos to its direct superstructure, with an update of pos to the position of the superstructure. When a result has to be recorded without changing the value of pos, we use the following variant yield :

To streamline the notation, we indicate that the machine is positioned on a direct subphrase t of a structure f (: : : t : : :) by writing s = f (: : : It : : :) for s = f (: : : t : : :) ^ pos =I. E.g. context(pos) = uop Ival denotes that the machine is positioned on the value val , computed for the expression exp which appeared as argument to uop. Similarly we write s = phrase(It) for s = phrase(t) ^ pos =I ^restbody=pos = t. When writing the rules we use the pattern matching notation which guarantees that the rules are tried to be applied, one at a time, in the order in which they appear in the text.

Expressions

The machine execJavaExpI in Fig. below formalizes for the imperative core of Java the condition in [18, x15.6] that all expressions are evaluated from innermost to outermost. For this purpose the current control is transfered, by updating pos, from unevaluated expressions to the appropriate subexpressions, until an atom (a literal or a variable) is reached. For binary expressions also the left-to-right evaluation strategy is taken into account, and for conditional expressions the condition is evaluated _rst. This reects also that as required in [18, x15.25.1], the value of a simple assignment expression is the value of its right hand side, which becomes bound under the name of the variable of the left hand side in the local environment. When the current

Execution of JavaI expressions

task restbody=pos requires to evaluate a context which is an atom or a compound expression all of whose relevant arguments are evaluated, this context is replaced by the (to be) computed value|which is determined for literals and for compound expressions by the JLS function de_ned in [18, x3.10] and for variables by the local environment function locals. For the evaluation of atoms the rule yield (result) is used, otherwise the rule yieldUp(result).

Statements

The machine execJavaStmI in Fig. below computes statements similarly to how execJavaExpI evaluates expressions. It follows the syntactical structure of the statement to be computed by transferring, through updates of pos, the current control from structured statements to the appropriate substatements, until the current statement has been computed normally or abrupts the computation.

This reects the following stipulations in [18, x14.2-10]: an empty statement, a type declaration and an empty block just terminate normally;an expression statement and a labeled statement terminate normally through evaluating the expression respectively through normally terminating the execution of the direct substatement; execution of a block statement follows the left-to-right evaluation strategy|started by executing the _rst of its substatements, and followed by the execution of the remaining substatements, in their textual order|and terminates normally when all the substatements have

Execution of JavaI statements

terminated normally; the execution of an if-else or a while statement is started by _rst evaluating the conditional expression. When the computation of the substatements terminate normally, the control switches to the statement which has to be computed next, namely by executing yieldUp(Norm) or, in case a while statement has to be iterated, yieldUp(body=up(pos)).

The execution of expressions or statements can be terminated through abruptions before all steps of their execution have completed normally. In JavaI only the computation of a statement can be abrupted, namely due to the execution, by execJavaStmI , of a jump statement (namely break or continue) which appears inside a labeled statement lab : s, with the e_ect that an element of Abr (here Continue(lab) or Break(lab)) becomes the term at the current position pos. Then the control propagates through all the enclosing statements up to the innermost enclosing labeled statement with label lab|the context conditions of Java guarantee the existence of such a labeled statement, which is called the jump target.

More precisely the machine looks at the superstructure restbody=up(pos) of the current position pos during whose execution the bruption did occur. If this enclosing structure is not a labeled phrase (so that it has to propagate the abruption), but also if it is a labeled phrase whose label does not agree with the label of the reason of abruption, then the abruption is propagated upwards. Otherwise, in case the reason is a Break(labb), the execution proceeds normally at the next phrase of the target, in case of a Continue(labc) the execution proceeds with the next iteration of the corresponding while statement, which is available in the method body at pos [18, x14.13,14.14,14.10]. This guarantees in particular that all statements complete abruptly which are passed through during the transfer of an abruption.

The concept of propagation is de_ned here in such a way that it can be extended easily to the abruptions in JavaC and JavaE where abrupt completion can also be due to return from procedure execution respectively to raising and handling of exceptions.:

propagatesAbr(phrase) = phrase 6= lab : s

Example (; CD). Abrupt transfer of control is illustrated in the following example:

l1: while (_exp) { ... l2: while (_exp) { ... break l1; // control goes to _ ... continue l1; // control goes to _ ... break l2; // control goes to ... continue l2; // control goes to _ ... } : : : } _ : : :

Derived language constructs

Derived language constructs

Table below contains some Java constructs that can be syntactically reduced to the core language. Other Java constructs like the do, for, switch statements as well as the postincrement operator loc++ and the postdecrement operator loc-- cannot be transformed to the core language. They have to be treated separately.

The JLS points out that the if statement without else' su_ers from the so-called dangling else problem'. Consider the following statement:

if (exp1) if (exp2) stm1 else stm2

This statement can be read in two di_erent ways:

Java reads it the _rst way. The problem disappears if one restricts the `if statement without else' to:

if (exp) block

Note, that block is surrounded with a pair of braces and cannot be an if statement.

For almost every binary operator bop there exists an assignment operator bop=. This operator is reduced in the following way (where A is the declared type of loc):

loc bop= exp is reduced to loc = (A)(loc bop exp)

or example, if the variable c is declared of type char, then

c += 32 is reduced to c = (char)(c + 32)

« Previous Topics
Static Semantics Of Java