Information Technology Reference
In-Depth Information
on the theory of
abstract interpretation
(cf. [3,4,5,6,31,37]). The point of this
approach is to replace the \full" semantics of a program by a simpler more ab-
stract version, which is tailored for a specic problem. Basically, an abstract
semantics is characterized by two objects:
data-flow facts
,and
data-flow func-
tions
. Typically, the data-flow facts are given by the elements of a complete (not
necessarily nite) lattice
C
of nite height, and the data-flow functions by trans-
formations [[
]] on these lattices. In practice, these functions are
monotonic
or
even
distributive
.
8
They dene the abstract semantics of elementary statements.
DFA then computes for every program point
:
n
a data-flow fact representing
valid data-flow information at
n
with respect to some
start assertion
. This is
a data-flow fact
, which is assured to be valid on calling the program
under consideration. Formally, this is characterized by the so-called
maximal-
xed-point
(
c
0
2C
) approach. It relies on a system of equations, which specify
consistency constraints which have to be obeyed by any reasonable annotation
of a flow graph with data-flow facts
MFP
c 2C
.
Equation System 3 (
MFP
-Equation System)
)=
c
0
if
n
=
s
info
(
n
u
f
[[ (
m; n
)](
info
(
m
))
j m 2 pred
(
n
)
g
otherwise
-approach is practically relevant, since Equation System 3 induces
an iterative computation procedure approximating its greatest solution denoted
by
info
c
0
. It denes the solution of the
The
MFP
MFP
-approach with respect to the start
assertion
c
0
2C
:
c
0
)=
info
c
0
(
The
MFP
-Solution:
8 c
0
2C8n2N: MFP
(
n
)(
n
)
MFP
-solution can eectively be computed, if the local semantic func-
tions are monotonic and the lattice is of nite height. This gives rise to consider
it the
algorithmic
solution of a DFA problem. Of course, this directly raises the
questions of its soundness and completeness.
The
Sound and Complete Analyses.
Soundness and completeness of the
-
approach are dened with respect to a second globalization of the abstract se-
mantics underlying the
MFP
MFP
-approach. Formally, it is given by the so-called
meet-over-all-paths
(
MOP
) approach. It has an operational flavour. Intuitively,
for every program point
n
it \meets" (intersects) all informations contributed
by some path
-approach mimics the eect of possi-
ble program paths, which intuitively reflects one's desires. Formally, the
p
reaching
n
.Thus,the
MOP
MOP
-
solution is dened as follows, where [[
p
]] denotes the sequential composition of
8
A function
f
i
8 c; c
0
2C:cvc
0
)f
(
c
)
vf
(
c
0
). It
:
C!C
is called
monotonic
u
ff
(
c
)
jc2C
0
g:
Monotonicity can
equivalently be characterized as follows:
8 C
0
C:f
(
u
C
0
)=
i
8C
0
C:f
(
is called
distributive
u
C
0
)
v
u
ff
(
c
)
jc2C
0
g
.
We prefer this characterization of monotonicity here because it directly pin-points
the dierence between monotonicity and distributivity.
Search WWH ::
Custom Search