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

of Boolean truth values is of nite height, and the
data-flow functions Cst true , Cst false ,and Id B are distributive. Hence, for both
problems the automatically generated xed point algorithm terminates with the
MFP

Obviously, the lattice B

-solution. Moreover, according to Theorem 3, it coincides as desired with
the corresponding MOP -solution. Hence, the instantiated MFP -algorithms are

sound and complete.
It is worth noting here that Equation System 1 and Equation System 2 are
direct specializations of Equation System 3. This is obvious for up-safety. For
down-safety, which requires a backward analysis of the program under consider-
ation, it gets obvious, when reversing the flow of control. This is the usual trick
in DFA to handle forward and backward problems in a uniform setting.
The main result of this section now is that the DFAs for up-safety and
down-safety induced by the appropriately instantiated generic

MFP -algorithm

are sound and complete. We have:

Theorem 4 (Soundness and Completeness).
The DFAs for up-safety and down-safety are sound and complete.

In the following sections we reconsider optimization in advanced settings
under the perspective of soundness and completeness. In particular, we focus
on the robustness of the placing strategy underlying the SE-transformation with
respect to setting and paradigm changes, and hence on the issue of reusability. We
start with re-considering the so-called interprocedural setting of optimization.

4 The Interprocedural Setting

Like intraprocedural optimization, also interprocedural one has its roots in the
imperative programming paradigm. In contrast to intraprocedual optimization,
however, it aims at capturing a program as a whole instead of treating its proce-
dures separately. Most importantly, this requires to take the eects of procedure
calls into account instead of making worst-case assumptions about them as in-
traprocedurally. Interprocedural optimization is thus much more ambitious than
intraprocedural one, however, generally also much more powerful.
In this section, we consider a setting where programs are composed of a
nite number of possibly mutually recursive procedures, which may have local
variables and value parameters. We assume that there is a unique procedure, the
main program , which cannot be called by other procedures. Local variables of
the main program are global variables of the remaining procedures of a program.
Moreover, we assume that procedures are not statically nested. This setting is
already complex enough for the purpose of this article.
Intuitively, reusing the placing strategy of the SE-transformation in the in-
terprocedural setting means that the interprocedural counterpart of the SE-
transformation, the ISE-transformation, inserts computations interprocedurally
as early as possible, i.e., at the interprocedurally earliest safe program points.
Figure 4(b) shows the eect of this transformation for the program of Figure