Information Technology Reference
In-Depth Information
=
null
)=
Γ,
{U} ¬
(
o
⇒{U}{
o.a
:=
se
}
[
πω
]
φ, Δ
writeAttribute
[
πo.a
=
se
;
ω
]
φ, Δ
where
o
is a schema variable matching program variables,
a
matches fields and
se
matches simple expressions without side-effects that can be directly translated
into a logic term. Fig. 5 shows a small excerpt of a sequent proof illustrating
symbolic execution. Finally, we discuss how dynamic dispatch of a method is
Γ
=
⇒{U}
.
.
Γ, {U}
(
b
=
TRUE
)=
⇒{U}
[
s1
]
φ, Δ
Γ, {U}
(
b
=
FALSE
)=
⇒{U}
[
s2
]
φ, Δ
φ, Δ
Γ
=
⇒
[
boolean b = (i>=0); if (b) then s1 else s2;
]
φ, Δ
Γ
=
⇒
[
if (i>=0) then s1 else s2;
]
φ, Δ
where
U
is the update
b
:=
if
Γ
=
⇒{U}
[
if (b) then s1 else s2;
]
(
i
≥
0)
then
(
TRUE
)
else
(
FALSE
)
Fig. 5.
Excerpt of a proof demonstrating symbolic execution
realized in the calculus. The rule for method invocation translates a dynamic
dispatch into a cascade of concrete method calls:
methodInvocation
Γ,
=
null
)=
{U} ¬
(
o
[
π
if (o instanceof
T
n
) res=o.m(se)@
T
n
;
else if (o instanceof
T
n−
1
) res=o.m(se)@
T
n−
1
;
...
else res=o.m(se)@
T
1
;
ω
]
φ, Δ
Γ
=
⇒{U}
[
π
res = o.m(se);
ω
]
φ, Δ
-
o
,
res
are schema variables for program variables.
-
res=o.m(se)@
T
are so called
method-body
statements. A method-body state-
ment is a place holder for an actual method body namely exactly the method
body of method
m
with the specified number of parameters as implemented
in class
T
.
-
T
1
,...,T
n
are all the subtypes of the static type of the program variable
against which
o
is matched and that contain an actual implementation of
the method
m
. As the most specific implementation has to be taken, the list
T
1
,...,T
n
fulfills the condition that for all 0
<i<j
⇒{U}
≤
n
:
T
i
T
j
.
4
Interleaving Symbolic Execution and Partial Evaluation
4.1 General Idea
Recall from Section 2.2 that a symbolic execution tree unwinds a program's
control flow graph (CFG). As a consequence, identical code is (symbolically) ex-
ecuted in many branches, however, under differing path conditions and symbolic
