Information Technology Reference
In-Depth Information
As usual, sequent rules are written in schematic form using schema variables
(pattern variables with matching restrictions):
Γ, φ, ψ
=
⇒
Δ
∗
Γ, φ
=
andLeft
close
φ, Δ
Here,
φ, ψ
(
Γ, Δ
) are schema variables that can be instantiated with any formula
(set of formulas). The sequent rule
andLeft
is applicable at any leaf sequent that
contains a disjunctively connected formula in its antecedent.
To handle formulas containing programs within our sequent calculus we aim
to model symbolic execution (see Sect. 2.2). Recall that a node in a symbolic
execution tree contains a program pointer to the next active statement, path
condition, and a symbolic state relative to which symbolic execution is executed.
Accordingly, nearly all sequent rules for programs work on a
first active statement
s
and a current
update
Γ, φ
∧
ψ
=
⇒
Δ
⇒
U
in the following general form of a conclusion:
[
π
s;
ω
]
φ, Δ
In addition,
π
stands for an inactive prefix containing labels, opening braces or
method-frames (see below) and
ω
for the remaining program. Path conditions
are represented by suitable formulas and accumulate in the antecedent
Γ
.
Symbolic execution in our
Γ
=
⇒{U}
-calculus can be roughly organized into two
phases. The first is the
rewriting phase
where the first active statement is re-
placed with an equivalent series of simpler statements. A typical rule is
DPL
Γ
=
⇒{U}
[
π
boolean b = nse; if (b) {s1} else {s2}
ω
]
φ, Δ
Γ
=
evalIfGuard
⇒{U}
[
π
if (nse) {s1} else {s2}
ω
]
φ, Δ
where
nse
is a schema variable matching any non-simple
-expression (basi-
cally, an expression that is neither a literal nor a program variable). As these
kind of rules are pure rewrite rules that can be applied in any possible syntactic
context (antecedent, succedent, box, diamond) we use the short form
ξ
PL
ξ
to
express that a term/program
ξ
is replaced with an equivalent term/program
ξ
:
if (nse) {s1} else {s2}
boolean b = nse; if (b) {s1} else {s2}
After the first active statement has been reduced to an elementary statement it
is translated into a first-order representation of its semantics with the help of
rules belonging to the second phase. For instance, if the first active statement
is a conditional whose guard is a simple expression (a program variable or a
boolean literal) then the rule
=
TRUE
)=
Γ,
{U}
(
b
⇒{U}
[
π
{s1}
ω
]
φ, Δ
=
FALSE
)=
Γ,
{U}
(
b
⇒{U}
[
π
{s2}
ω
]
φ, Δ
ifElseSplit
[
π
if (b) {s1} else {s2}
ω
]
φ, Δ
splits the current proof branch into two branches, one for the case when the
guard evaluates to true, and the other covering the
else
case. Further important
representatives of the rules in this phase are assignment rules like
Γ
=
⇒{U}
