Information Technology Reference
In-Depth Information
--- Stack loop and transform while expression into while continuation
eq k((while E S) -> K) lstack(Lstack)
= k(while(E,S) -> popLStack -> K) lstack(while(E,S) -> K, Lstack) .
--- A while continuation is transformed into an if-then-else
eq k(while(E,S) -> K) = k(E -> if(S while ( E , S ),{}) -> K) .
--- Add semantics for popLStack
eq k(popLStack -> K) lstack(LItem,Lstack) = k(K) lstack(Lstack) .
Fig. 3.
Continuation-based equations for while statement
--- The state is restored from the loop stack
eq k(break -> K) lstack(while(E,S) -> K', Lstack) = k(K') lstack(Lstack).
Fig. 4.
Continuation-based equations for while break statement
The if-then-else statement is shown in Figure 2. The semantics of while state-
ments (loops) is specified in Figure 3, where the term
while E S
denotes the Java
iteration statement, the term
while
(
E
,
S
) denotes both the while continuation
and the while statement that is expressed in terms of the
if
(
S
,
S
) continuation,
and
lstack
denotes a stack of loops currently being executed, which is needed
for a proper control of the Java
break
statement. Figure 4 shows the semantic
specification of the
break
statement, that simply pops the stack of loops. This
is important, since it can also abruptly change the information flow. Method
calls are not shown in this paper; their semantics is simply defined by eager
evaluation of all arguments of the method (whose values are stored in new mem-
ory locations) and by creating a new local environment that contains location
assignments for formal method parameters and local variables. Due to space
limitations we do not discuss heap manipulation here. We refer the reader to
[18] for further details.
The following example illustrates the mechanization of the Java semantics.
Example 2.
Consider again the Java program of Example 1 and two program
executions, respectively fed with 5000 and 10000 for the initialization parameter
initbalance
. Note that the corresponding initial states are indistinguishable at
the
Low
confidentiality level (e.g. the only
Low
-labeled variable,
extraService
,
is set to
false
in both of them). The Maude command
search
provides built-in
breadth-first search. We ask for the final Java program state of each execution
trace (actually, in order to visualize the results, we show the output of
println
Java instructions). The Maude terms
EX1-MAUDE
and
EX2-MAUDE
stand for the
Java program with the corresponding initial call (for input value 5000 and 10000,
respectively), which are compiled into a Maude expression by using a suitable
Java wrapper
2
:
search in PGM-SEMANTICS :
java((preprocess(EX1-MAUDE) noType . 'main < new string [i(0)] > noVal))
=>! JO:Output .
Solution 1 JO:Output --> pl(bool(false))
No more solutions.
2
See
http://fsl.cs.uiuc.edu/index.php/Rewriting_Logic_Semantics_of_Java
