Information Technology Reference
In-Depth Information
eq k((E > E') -> K) = k((E, E') -> > -> K) . ---Evaluate arguments
eq k((int(I), int(I')) -> > -> K) = k(bool(I > I') -> K) . ---Resolve
Fig. 1.
Continuation-based equations for the Java greater-than operator on integers
--- Evaluates boolean expression keeping the then and else statements
eq k((if E S else S') -> K) = k(E -> (if(S, S') -> K)) .
eq k(bool(true) -> (if(S, S') -> K)) = k(S -> K) .
eq k(bool(false) -> (if(S, S') -> K)) = k(S' -> K) .
Fig. 2.
Continuation-based equations for if-then-else statement
u, v
(which denote Java program states) are rewritten (at the top position, see
[12]) by using
r
, which is either a rule in
R
Java
or an equation in
Δ
Java
(both
of which are applied modulo
B
Java
). We simply write
u
→
Java
v
when the ap-
→
Java
the extension of
plied rule or equation is irrelevant. We denote by
→
Java
→
Java
to multiple rewrite steps (i.e.,
u
v
if there exist
u
1
,...,u
k
such that
u
→
Java
u
1
→
Java
u
2
···
u
k
→
Java
v
).
R
Java
is defined on terms of a concrete sort
State
,with
the main state attributes (represented by means of constructor symbols of the
algebraic type
State
)suchas
fstack
for handling function calls,
lstack
for han-
dling loops,
env
for assignments of variables to memory locations, and
store
for
assignments of memory locations to their actual values. They define an algebraic
structure that is parametric w.r.t. a generic sort
Value
that defines all the possible
values returned by Java functions or stored in the memory. For instance, the
int
and
bool
constructor symbols describe Java integer and boolean values and are
defined in Maude as “
op int
:
Int
The rewrite theory
Value
.
”,
where
Int
and
Bool
are the internal built-in Maude sorts that define integer
and boolean data types. Intuitively, equations in
Δ
Java
and rules in
R
Java
are
used to specify the changes to the program state (i.e., the changes to the mem-
ory, input/output, etc). Since we consider only deterministic Java programs, our
specification of the Java semantics in rewriting logic contains only equations
and no rules. The reader can find a RWL specification of the semantics of a
programming language with threads in [18,1,2].
The semantics of Java is defined in a
continuation-based style
[18] and specified
in Maude itself. Continuations maintain the control context, which explicitly
specifies the next steps to be performed. The sequence of actions that still need
to be executed are stacked. We use letters
K
,
K
to denote continuation variables,
letters
E
,
E
to denote expressions to be evaluated, and
Val
,
Val
to denote values
(i.e., the result of evaluating an expression). Once the expression
e
on the top of
a continuation (
e
->
k
) is evaluated, its result will be passed on to the remaining
continuation
k
. For instance, in Figure 1, the Java greater-than operation on Java
integers is specified by using continuations, where
k
is the constructor symbol
used to denote a continuation,
->
is the constructor symbol used to concatenate
continuations,
bool
is the constructor symbol used to denote a Java boolean
data, and
int
is the constructor symbol used to denote a Java integer number.
→
Value
.
”and“
op bool
:
Bool
→
