Optimization Under the Perspective of Soundness, Completeness, and Reusability - Correct System Design: Recent Insights and Advances - page 287

the data-flow functions associated with the edges of p .Note,if p is the empty

path, [[ p ]] equals the identity on C .

u f [[ p ]] ( c 0 ) j p 2 P [ s ;n ] g

The MOP -Solution: 8 c 0 2C8n2N: MOP ( n )( c 0 )=

In terms of program verication, the MOP -solution at a program point n can

be considered the strongest post-condition at with respect to the pre-condition

c 0 at the program's entry s . This gives rise to consider the

n

-solution the
specifying solution of a DFA problem. 9 Consequently, we dene: the algorithmic
MFP

MOP

MOP

-solution of a DFA problem is sound , if it is a lower bound of the -

MOP

solution. It is complete , if it coincides with the -solution. In DFA these two

properties are usually called safety and coincidence of the

MFP

-solution with

respect to the -solution (cf. [9,10]).

The following two theorems proposed by Kildall [10], and Kam and Ullman
[9], which are known as Safety Theorem (Theorem 2) and Coincidence Theorem
(Theorem 3), give sucient conditions for the soundness and completeness of
the

MOP

-solution. These theorems are used
in practice for proving the soundness and completeness of a DFA. Note that they
do not rely on the nite height condition of the lattice under consideration. This
constraint is only required to guarantee the eectivity of the xed point process
computing the

MFP -solution with respect to the MOP

MFP -solution.

Theorem 2 (Soundness).
The MFP -solution is sound for the MOP -solution, i.e., it is a safe approximation

of the MOP -solution, in symbols 8 n 2 N: MFP ( n ) v MOP ( n ) ,ifthesemantic

functions [[ e ]] , e 2 E , are all monotonic.

Theorem 3 (Completeness).
The

MFP -solution is complete for the MOP -solution, i.e., it coincides with the

MOP -solution, in symbols 8 n 2 N: MFP ( n )= MOP ( n ) , if the semantic func-

tions [[ e ]] , e 2 E , are all distributive.

Note that distributivity implies monotonicity. Thus, on the analysis level
of optimization completeness implies soundness. The analogy of soundness and
completeness in program verication and program analysis is thus not really
one-to-one.
From the perspective of reuse, and hence, for the construction of optimizing
compilers, it is most important that the procedure computing the

MFP

-solution
can be generically organized. Hence, it can be reused. Feeding the generic

MFP

-
algorithm with instances of data-flow facts and data-flow functions yields auto-
matically the incidental concrete DFA algorithm. This is illustrated in Figure 3.
The principle showing up in this gure is the basis of the intraprocedural version
of the DFA&OPT- tool kit, a DFA generator (cf. [11,24]).

9 Unfortunately, its denition does generally not induce an eective computation pro-
cedure. Think e.g. of loops in a program, which cause the existence of an innite
number of paths reaching a specic program point.

M eta Frame