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.
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[]
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:
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.
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
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, (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 ]]
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, (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
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
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