Transition rules for JavaO - JVM

Vocabulary of JavaO

The following static functions look up compile-time information in the environment:

The function instanceFields calculates the set of instance _elds declared by the speci_ed class and all of its superclasses (if any). Hence D=_eld belongs to instanceFields(C) i_ C _h D and _eld is an instance _eld of D.

Example (; CD). Consider the following two classes:

Then instanceFields(B) = [A=x; A=y; B=x]. An object of type B has _elds A/x, A/y, B/x. The _eld A/z is static and therefore not an instance _eld.

The function defaultVal maps types to their default values as speci_ed in [18,x4.5.4]. The function type returns the declared type of the _eld in the class.

The function lookup yields the class where the given method speci_cation is de_ned with respect to the class hierarchy. The function lookup(A;B=msig) is computed as follows:

  1. If class A contains a non abstract declaration of msig and a) B is an interface, or b) A=msig overrides B=msig (cf. Def below), then lookup(A;B=msig) = A.
  2. Otherwise, if C is the direct superclass of A, then lookup(A;B=msig) = lookup(C;B=msig).
  3. Otherwise, A = Object and lookup(A;B=msig) = undef .

Example below. This example illustrates some details of the dynamic method lookup. Consider the following two packages:

The method p:A=m() is not visible in package q. Therefore the method q:B=m() does not override p:A=m(). Although the variable x contains at run-time a reference of type q:B, the output of the program is p. If the method p:A=m() is declared public, then the output of the program will be q.

An object is an instance of a non abstract class. Objects are represented by references (pointers). References belong to the dynamic universe Ref . We extend the universe Val in JavaO to include references and the value null .

type Val = : : : j Ref j null

To model the dynamic state of objects, we have to reserve storage for all instance variables and have to store to which class an object belongs. The dynamic function heap records the class together with the _eld values of an object. The function classOf returns the class of the object that is referred to by the reference.

More precisely, if heap(ref ) = Object(C; _elds), then _elds is a _nite map which assigns a value to each _eld in the list instanceFields(C).

Transition rules for JavaO

The initial state and the termination conditions of JavaO are the same as for JavaC. Since JavaO has only new expressions and no new statements, the rules for JavaO extend only the expression evaluation rules of JavaI and JavaC.

Execution of JavaO expressions

Execution of JavaO expressions

An additional rule extends exitMethod, describing the special case of a return from a constructor initialization method.

The expression evaluation machine execJavaExpO de_ned in Fig. below passes the control from object related expressions to the evaluation of the corresponding object expression, namely for _eld access, _eld assignment, type check, type cast, instance method invocation and creation of a parametrized new class instance (if the class is initialized). The machine execJavaExpO treats this the way execJavaExpI handles local variables, upon invoking an instance method it binds the value of this keyword to the reference for the object for which the instance method is invoked [18, x15.7.2]. The expression null is a literal with value null .

execJavaExpO treats the access and the assignment to instance _elds similarly to how execJavaExpI deals with local variables, checking in addition that the previously computed object, pointed to by the target reference, is not null . The value of the computed expression, in the case of a _eld access, is the value _elds(f ) which is stored in the heap for the object pointed to by the target reference ref [18, x15.10]; it is described by the function getField below. In the case of a _eld assignment, the value of the computed expression is the value of the right-hand side of this assignment [18, x15.25] which, using setField, is stored in the heap to the _eld for the object pointed to by the target reference.

For type check and cast expressions execJavaExpO passes the dynamic type condition of the computed subexpression up to the expression. The semantics of instance method calls as de_ned by execJavaExpO [18, x15.11] is similar to that de_ned by execJavaExpC for static method calls in that the evaluation of the arguments of the call (which includes the binding of the reference target to this) is guaranteed to happen before the values of these arguments are bound through invokeMethod to the method parameters. In addition, before applying invokeMethod, the machine checks that the target reference is de_ned; it determines dynamically the method body to be executed [18,x15.11.4].

For the creation of a parametrized new class instance, execJavaExpO guarantees that the class get initialized before the parameter values are evaluated in the left-to-right order. Only then a reference to the newly created object of the speci_ed class type is stored on the heap, together with new instances (instantiated with their default values) of all the _elds declared in the speci_ed class and its superclasses [18, x15.8], and the constructor method is invoked.

The exitMethod rule has to be extended for constructors. The result of a constructor invocation with new is the newly created object which is stored in the local environment as value for this.

The e_ect of the execJavaExpO-extension of the exitMethod rule is the same as if during the parsing and elaboration phase a `return this' is inserted at the end of each constructor.

All rights reserved © 2018 Wisdom IT Services India Pvt. Ltd Protection Status

JVM Topics