Information Technology Reference
In-Depth Information
program is abstracted. In the previous example, the control abstraction does not
allow to decide whether the program may reach a state with
x<
0.
Unifying the concepts.
Intensionality and abstraction are different and inde-
pendent concepts that can be unified by means of abstract interpretation [9].
Abstract interpretation is a general theory that defines how a correct fixpoint
calculation on a lattice approximates a fixpoint calculation on a different lattice.
To unify intensionality and abstraction, we start by considering, for a pro-
gram
p
and a set of initial states
I
, the function f(
S
)
de
=Post(
p, S
)
I
,which
is a continuous function over the complete powerset lattice of program states.
The least fixpoint of f(
S
) represents the set of the reachable state space of the
program. It exists and is equal to
k≥
0
Post
k
(
p, I
) . The fully exhaustive reach-
ability procedure is therefore sound, in that it calculates this fixpoint whenever
the iterative procedure converges.
We now consider a structure
A
composed by a different complete lattice
∪
T
A
,
whose elements are interpreted as sets of states, together with a “translation”
of Post into
T
A
. More precisely,
A
=(
T
,
−
,
Post
A
)
,
where
-
T
=(
T
,
,
⊥
,
,
) is a complete join-semilattice,
-
−
:
T
→P
(
S
) is monotone and preserves bottom and top (
=
S
,
),
-
Post
A
:
P
⊥
=
∅
×
T
→
T
is monotone and has the property:
Post(
p,
I
A
)
⊆
Post
A
(
p, I
A
)
.
Intuitively,
−
assigns a meaning (a set of program states) to every element of
T
,andPost
A
overapproximates Post over
T
.
The algorithm described in Figure 6 implements the algorithm for full exhaus-
tive exploration from Figure 2 on
, and calculates a safe overapproximation of
S
into
S
A
that upon convergence is a safe overapproximation of the reachable
state space. Indeed, it can be easily proved that
4
, whenever
I
A
overapproximates
I
(i.e.,
I
T
⊆
I
A
), it is:
Post
k
(
p, I
)
Post
A
(
p, I
A
)
⊆
0
≤k<n
0
≤k<n
and:
Post
k
(
p, I
)
Post
A
(
p, I
A
)
⊆
.
k≥
0
k≥
0
implies that
S
A
∈T
S
A
⊆
4
We must take into account that monotony of
−
S
A
∈T
S
A
, for all
T ⊆
T
.
Search WWH ::
Custom Search