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

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

Now, we dene: the algorithmic IMFP

IMOP -solution. It is complete ,

if it coincides with the -solution. The Interprocedural Safety Theorem 5

and the Interprocedural Coincidence Theorem 6 give sucient conditions for the
soundness and completeness of the

IMOP

-solution [28]. Note that the niteness
condition on the height of the function lattice of the data-flow fact lattice

IMFP

C

is
only required to guarantee the eectivity of the xed point process computing
the

IMFP

-solution.

Theorem 5 (Interprocedural Soundness).
The IMFP -solution is sound for the IMOP -solution, i.e., it is a safe approxi-

mation of the IMOP -solution, in symbols 8 n 2 N: IMFP ( n ) v IMOP ( n ) ,ifthe

semantic functions [[ e ]] , e 2 E , and the return functions are all monotonic.

Theorem 6 (Interprocedural Completeness).
The

IMFP IMOP

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

IMOP 8 n 2 N: IMFP n IMOP n

the -solution, in symbols ( )= ( ) , if the semantic

functions [[ e ]] , e 2 E , and the return functions are all distributive.

After these preliminaries we can now apply the framework introduced above
to the computation of the program properties involved in the ISE-transformation.
In fact, the denitions of interprocedurally earliest safe program points as well
as those of interprocedurally down-safe and interprocedurally up-safe program
points can straightforwardly be derived from their intraprocedural counterparts.
The specications of the corresponding DFAs for interprocedural up-safety and
down-safety have been given in detail in [24], and we thus omit recalling them
here. The specications of these DFAs satisfy both the eectivity requirements
of the -approach, and the completeness requirements imposed by the Com-

pleteness Theorem 6.
Hence, the analyses for up-safety and down-safety can successfully be en-
hanced to the interprocedural setting. As mentioned before, this is necessary for
the successful reuse of the placing strategy underlying the SE-transformation in
the interprocedural setting. In the following section we will investigate whether
it is sucient, too. 10

IMFP

4.2 Transformation Level

In analogy to intraprocedural PRE, we dene soundness and completeness of
interprocedural PRE ( IPRE ) as semantics preservation and computational opti-
mality. This is rather straightforward, but it directly allows us to expose a most
10 In [14] the soundness and completeness theorems have been given for a more general
setting including also formal procedure parameters and formal reference parameters.
Even for this more general setting the interprocedural versions of the DFAs for up-
safety and down-safety satisfy the eectivity and completeness requirements of the
IMFP -approach.