Information Technology Reference
In-Depth Information
ExploreAbstract(
p
,
I
,
O
,
A
):
--
de
=(
T ,
−
,
Post
A
)
S
A
:= some
I
A
from
T
s.t.
I ⊆
I
A
O
A
:= some
O
A
from
T
s.t.
O
A
⊆ O
exact := (
S
A
=
I
)
A
∧
(
O
A
=
O
)
loop:
if
S
A
O
A
:
if exact return INCORRECT else return INCONCLUSIVE
S
A
:=
Post
A
(
p, S
A
)
exact := exact
∧
(
S
A
=Post(
p,
S
A
)
)
S
A
S
A
if
return CORRECT
S
A
S
A
S
A
:=
Fig. 6.
Abstract state space exploration
assignment. It also computes a
path condition
associated to each symbolic state.
The path condition is a predicate that is computed as the logical “and” of all the
guards in the sequence of assignments used to produce the state, and represents
the assumption on the initial values of the variable for the state to exist. When
a symbolic state has a contradictory path condition, it is discarded.
We can formalize symbolic execution by defining symbolic states as members
of the set
S
sy
de
=(
X
E
, whose elements are mappings of variables
X
to
expressions
E
joint with a path condition
E
. For example, the symbolic state
(
→
E
)
×
,x>
0) represents a set of concrete states where the value of
x
is
twice plus four its initial value, which in turn was an arbitrary positive integer.
The initial symbolic state is a pair (id
,init
), where id is the identity map on
variables (i.e., maps each variable to itself) and
init
is an expression having
I
as
extension
, where the extension of an expression
e
{
x
→
2
x
+4
}
∈
E
is the set
e
of all and
only the states where the expression evaluates to true:
de
=
e
{
s
∈
S
|
e
s
=
true
}
,
and
=
I
.
To define the meaning of sets of symbolic states, we first introduce an auxiliary
translation function:
init
de
=
(
σ, γ
)
∃
X
0
.γ
[
X
0
/
X
]
∧
X
=
σ
[
X
0
/
X
]
.
The translation essentially states the existence of an initial (program) state that
satisfies the guard of a symbolic state, and is transformed by the associated
symbolic map into the final (program) state. As an example,
(
{x →
2
x
+4
},x>
0)
=
∃x
0
.x
0
>
0
∧ x
=2
x
0
+4
.
We can now define the meaning of a set of symbolic states as the function
−
P
→P
:
(
S
sy
)
(
S
) defined as follows:
de
=
S
sy
s
sy
,
s
sy
∈S
sy
Search WWH ::
Custom Search