ESCJ 9: Java to Guarded Commands Translation

By Rustan and Raymie, 11 April 1997.

This note describes a translation of Java statements into a guarded command-like language. This note is not about resolution of names in Java, so we assume where convenient that names have been mangled to make them distinct. In particular, we assume the names of types, fields, and methods have been so mangled. In the case of methods, mangling takes care of overloading by taking into account the types of formals.

Java-like AST

In our grammar, V is the set of names that can be used for parameters and local variables; F is the set of names used for methods and fields (both static and non-static); and T is the set of names used for the types created by Java class and interface declarations.

K: // All types, including built-ins, arrays, classes and interfaces
    int | bool | ... // built-ins
    T   // Classes and interfaces
    K[] // arrays

S:
    (block N (V T)* S*) // N ::= name, V ::= variable
    (if E S S)
    (while-do N E S)
    (do-while N S E)
    (for N (V T)* (E*) E (E*) S)
    (continue N)
    (break N)
    (skip)
    (eval E)
    (S catch ((V T) S)*)
    (S finally S)
    (return E)
    (throw E)
    (switch N E ((case C)* S)* (default S)) // C ::= constant
    (synchronized E S)
    (supercons F E_1 E_2 .. E_n) // Only appears @ start of constructor

L: // Location, i.e., left-hand sides of exprs
    V
    E[E]
    E.F // F ::= field-name

E:
    this
    L
    C // Literal
    (<un-op> E)
    (<bin-op> E E)
    (if E E E)
    (:= L E)
    (new:= L <bin-op> E) // Assign E to L, return new value of L
    (old:= L <bin-op> E) // Assign E to L, return old value of L
    (new T E*)
    (callstatic F E*)
    (callvirtual T F E*) // Dynamically-dispatched method invocation (invoked
                         // on something whose static type is T)
    (callspecial T F E*) // Covers super.m() & invocation of private methods
    (newarray K E*) // K is element type
    (instanceof E K) // For K must be either T or K[]
    (cast K E) // For K must be either T or K[]

Guarded-command-like syntax

Our translation targets a guarded command language whose syntax is given below. Note that the syntax of this language overlaps the syntax of the above language in that it uses the sets N, V, and C.

B:
H := X
skip
raise
wrong
var V* B rav
while X do B od
B ; B
B ! B
B [] B
X --> B

if X then B_c else B_a fi == X --> B_c [] ~X --> B_a
try N B yrt ==                B ! (ec = N --> skip [] ec ~= N --> raise fi)
assert X ==                   X --> skip [] ~X --> wrong
break N ==                    ec = N; raise

H:
V
X.F
X[X]

X:
H
C
X <bin-op> X
<un-op> X

In our translations below, we assume the existence of a number of global variables:

ec When a guarded command exception is raised (using the raise command), the variable ec (exception code) is used to indicate whatthe nature of the exception.
result The variable "result" is used to communicate results from a method back to its caller.
tc The variable tc is used to communicate to constructors the typecode of the result they are supposed to return.
LL This is the set of locks held by the current thread.

Note that these special variables are members of V, but they cannot appear in Java program text; all but the last can appear in Java specs.

In addition, we assume the existence of a function named typecode. If "." is an object, then typecode(.) returns the typecode corresponding to the runtime type of the object. If "." is a type, typecode(.) returns the typecode corresponding to the type.

Translating E

Idea: D[[ V, E ]] generates a guarded-command statement that assigns the result of E to V after computing the side-effects of E. If an exception is raised while these side-effects are being computed, then no asignment is made to V (i.e., V remains unchanged). V should not be a variable that's mentioned either in E or in the translation of E. An implication of this restriction is that V cannot be any of the special, global variables such as result.

The translations below introduce intermediate variables. We assume these variables are fresh in that they are not V and they are contained in E.

D[[ V, C ]] =
V := C

D[[ V, this ]] =
V := this

D[[ V_1, V_2 ]] =
V_1 := V_2

D[[ V, E_1[E_2] ]] =
var x y
    D[[ x, E_1 ]];
    D[[ y, E_2 ]];
    V := x[y]
rav

D[[ V, E.F ]] =
var x
D[[ x, E ]];
V := x.F
rav

D[[ V, (<un-op> E) ]] =
var x
D[[ x, E ]];
V := <un-op> x
rav

D[[ V, (E_1 <bin-op> E_2) ]] =
var x y
    D[[ x, E_1 ]];
    D[[ y, E_2 ]];
    V := x <bin-op> y
rav

D[[ V, (if E_t E_c E_a) ]] =
var b
D[[ b, E_t ]];
if b then D[[ V, E_c ]] else D[[ V, E_a ]] fi
rav

Intermission: dealing with L when on left-hand side

X[[ C, V ]] = C(V)

X[[ C, E.F ]]] =
var y D[[ y, E ]]; C(y.F) rav

X[[ C, E_1[E_2] ]] =
var y z D[[ y, E_1 ]]; D[[ z, E_2 ]]; C( y[z] ) rav

(End of intermission.)

D[[ V, (:= L E) ]] =
X[[ \lambda l . var x . D[[x, E]]; l := x; V := l, L ]]

D[[ V, (new:= L <bin-op> E) ]] =
X[[ \lambda l . var x y . y := l; D[[x, E]]; l := y <bin-op> x; V := l, L ]]

D[[ V, (old:= L <bin-op> E) ]] =
X[[ \lambda l . var x y . y := l; D[[x, E]]; l := y <bin-op> x; V := y, L ]]

Intermission: specifications

req R mod w ens Q except-ensures E

where w is a set of program variables, R is a one-state predicate, and Q and E are two-state predicates. A two-state pred is allowed to mention primed versions of variables in w and also result' (not result).

(End of intermission.)

D[[ V, (callproc T F E_1 E_2 .. E_n) ]] = // The following four are basically
D[[ V, (callproc P E_1 E_2 .. E_n) ]] =
D[[ V, (invoke T F E_1 E_2 .. E_n) ]] =   // the same...
var f_1, f_2, .., f_n // f_i are the names of the formals
    D[[f_1, E_1]]; D[[f_2, E_2]]; ...; D[[f_n, E_n]];
    assert R;
    var w', ec', result'
         ec' = $return$ /\ Q --> w := w'; V := result'
      [] ec' = $throw$ /\ E --> w := w'; result := result'; ec := ec'; raise
    rav
rav

D[[ V, (new T E_1 E_2 .. E_n) ]] =
var $tc$, f_1, f_2, .., f_n // f_i are the names of the formals
    D[[f_1, E_1]]; D[[f_2, E_2]]; ...; D[[f_n, E_n]];
    $tc$ := typecode[[T]];
    assert R;
    var w', ec', result'
         ec' = $return$ /\ Q --> w := w'; V := result'
      [] ec' = $throw$ /\ E --> w := w'; result := result'; ec := ec'; raise
    rav
rav

D[[ V, (newarray K E_1 E_2 .. E_n) ]] =
var a, alloc', l_1, .., l_n
    D[[ l_1, E_1 ]]; D[[ l_2, E_2 ]]; ..; D[[ l_n, E_n ]];
    Jumbo[[n]] --> V := a; alloc = alloc'
rav
where Jumbo[[ n ]] =
    succeeds(alloc,alloc')
    ~alloc[a] & alloc'[a] & a.length = l_1
    typecode[a] = K[][]..(n of these)..[]
    \forall i_1 :
      ~alloc[a[i_1]] & alloc'[a[i_1]] & a[i_1].length = l_2
      typecode[a[i_1]] = K[][]..(n-1 of these)..[]
      \forall j_1 : a[i_1] = a[j_1] ==> i_1 = j_1
      \forall i_2 :
        ~alloc[a[i_1][i_2]] & alloc'[a[i_1][i_2]] & a[i_1][i_2].length = l_3
        typecode[a[i_1][i_2]] = K[][]..(n-2 of these)..[]
        \forall j_1,j_2 : a[i_1][i_2] = a[j_1][j_2] ==> i_1 = j_1 & i_2 = j_2
        ...
          \forall i_{n-1} :
             ~alloc[a[i_1][i_2]...[i_{n-1}]]
             alloc'[a[i_1][i_2]..[i_{n-1}]]
             a[i_1][i_2]..[i_{n-1}].length = l_n
             typecode[a[i_1][i_2]..[i_{n-1}]] = K[]
             \forall j_1,j_2,..,j_n :
                a[i_1][i_2]..[j_n] = a[j_1][j_2]..[j_n]
                  ==> i_1 = j_1 & i_2 = j_2 & .. & i_n = j_n
             \forall i_{n-1} :
               a[i_1][i_2]..[i_{n-1}][i_n] = "zero-equiv for K"

D[[ V, (instanceof E K) ]] =
var x
D[[ x, E ]];
V := typecode(x) = typecode(K)
rav

D[[ V, (cast K E) ]] =
var x
    D[[ x, E ]];
    if (typecode(x) ~= typecode(K)) then
      ec = $throw$;
      result = ...instance of runtime exception...;
      raise
    fi;
    V := x
rav

Translating S

D[[ S ]] translates a Java statement into a guarded-command statement. We assume again that variables introduced in transltion are fresh.

D[[ (skip) ]] =
skip

D[[ (eval E) ]] =
var tmp D[[ tmp, E ]] rav

D[[ (block N (V_1 T_1) (V_2 T_2) .. (V_m T_m) S_1 S_2 .. S_n) ]] =
try N
    var V_1 V_2 .. V_m
      D[[ S_1 ]]; D[[ S_2 ]]; ...; D[[ S_n ]]
    rav
yrt

D[[ (if E S_c S_a) ]] =
var b
D[[ b, E ]];
if b then D[[ S_c ]] else D[[ S_a ]] fi
rav

D[[ (while-do N E S) ]]
try N
    var b
      D[[ b, E ]];
      while b do try N$continue D[[ S ]] yrt; D[[ b, E ]] od
    rav
yrt
// Note: N$continue is the concatenation of N with "$continue"

D[[ (do-while N S E) ]]
try N
    var b
      b := true;
      while b do try N$continue D[[ S ]] yrt; D[[ b, E ]] od
    rav
yrt

D[[ (for N (V_1 T_1) .. (V_n T_n)
           (E_i1 E_i2 .. E_im)
           E_t
           (E_u1 E_u2 .. E_uk)
        S) ]] =
try N
    var V_1 .. V_n, tmp, b
      D[[ tmp, E_i1 ]]; D[[ tmp, E_i2 ]]; ...; D[[ tmp, E_im ]]
      E[[ b, E_t ]]
      while (b) do
        try N$continue D[[ S ]] yrt;
        D[[ tmp, E_u1 ]]; D[[ tmp, E_u2 ]]; ...; D[[ tmp, E_uk ]];
        E[[ b, E_t ]]
      od
    rav
yrt

D[[ (break N) ]] =
break N

D[[ (continue N) ]] =
break N$continue

D[[ (return E) ]] =
var x
    D[[ x, E ]];
    result := x;
    ec = $return$;
    raise
rav

D[[ (throw E) ]] =
var x
    D[[ x, E ]];
    result := x;
    ec = $throw;
    raise
rav

D[[ (S_1 finally S_2) ]] =
(D[[S_1]] ! var ec0, result0
                 ec0 = ec; result0 = result;
                 D[[S_2]];
                 ec = ec0; result = result0;
                 raise
              rav); D[[S_2]]

D[[ (S catch ((V_1 T_1) S_1) ((V_2 T_2) S_2) .. ((V_n T_n) S_n)) ]] =
D[[ S ]] !
var tcr
    tcr := typecode(result);
    if (ec == $throw$) then
      if (tcr = typecode(T_1)) then V_1 := result; D[[ S_1 ]]
        else if (tcr = typecode(T_2)) then V_2 := result; D[[ S_2 ]]
        ...
        else if (tcr = typecode(T_n)) then V_n := result; D[[ S_n ]]
        else raise
      fi ... fi fi
     else raise
    fi
rav

D[[ (switch N E ((case C_11) (case C_12) .. (case C_1n_1) S_1)
                ((case C_21) (case C_22) .. (case C_2n_2) S_2)
                ...
                ((case C_m1) (case C_m2) .. (case C_mn_m) S_m)
                (default S_d)) ]] =
var e
    D[[ e, E ]];
    try N
      if (CL1) then D[[ S_1 ]] else skip fi;
      if (CL1 \/ CL2) then D[[ S_2 ]] else skip fi;
      ...
      if (CL1 \/ CL2 \/ ... \/ CLm) then D[[ S_m ]] else skip fi;
      D[[ S_d ]]
    yrt
rav
    where CLi = (e = C_i1 \/ e = C_i2 \/ ... \/ e = C_in_i)
Alternative:
var e
    D[[ e, E ]];
    try N
      (CL1 /\ ~CL2 /\ ... /\ ~CLm) --> D[[(block S_1 S_2 ... S_m S_d)]]
      [] (~CL1 /\ CL2 /\ ~CL3 /\ ... /\ ~CLm) --> D[[(block S_2 ... S_m S_d)]]
      ...
      [] (~CL1 /\ ~CL2 /\ ~CL3 /\ ... /\ ~CLm) --> D[[S_d]]
    yrt
rav

Note: Alternative looks better because (a) the number of paths through the try seems to be O(m) rather than O(2^m) (assuming D[[S_i]] translates into a single path) and (b) in most cases S_i ends in a (break) statement, allowing us to easily optimize the bodies of each path (specifically, each path is more likely to look like "D[[S_i]]" then it is to look like "D[[(block S_i S_i+1 ... S_m S_d)]]"). D[[ (synchronized E S) ]] =
var e, LLold
    D[[ e, E ]];
    assert e != null /\ (e \in LL \/ sup(LL) < e);
    LLold := LL;
    LL := LL \cup { e };
    ((D[[ S ]]; LL := LLold) ! (LL := LLold; raise))
rav

D[[ (supercons F E_1 E_2 .. E_n) ]] =
var f_1, f_2, .., f_n // f_i are the names of the formals
    D[[f_1, E_1]]; D[[f_2, E_2]]; ...; D[[f_n, E_n]];
    assert R;
    var w', ec', result'
         ec' = $return$ /\ Q --> w := w'; this := result'
      [] ec' = $throw$ /\ E --> w := w'; result := result'; ec := ec'; raise
    rav
rav

Legal Statement Privacy Statement