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