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

necessary recomputations of values at run-time. This is achieved by replacing
the original computations of a program by temporaries which are initialized at
suitable program points as illustrated in Figure 1(a) and Figure 1(b).

a) b)

a := ...

a := ...

h := a+b

x := a+b

x := h

h := a+b

z := a+b z := h

x := a+b z := a+b x := h z := h

b := a+b b := h

Original Program Computationally Optimal Program

Fig. 1. Illustrating the essence of partial redundancy elimination.

Obviously, an optimization must obey some minimum requirements in order
to be reasonable. It must not aect the semantics or decrease the performance of
a program. Under these constraints, it should produce a program which is better
than any other program resulting from an optimization of the same transfor-
mation class. In optimization these requirements are usually called admissibility
and optimality of an optimization.
Though it is not common in program optimization to rephrase admissibil-
ity and optimality in terms of program verication, they can be rephrased as
soundness and completeness. Considering partial redundancy elimination for il-
lustration, a PRE-transformation is sound (i.e., admissible), if (1) inserted state-
ments do not introduce the computation of a new value on any path, and if (2)
temporaries replacing original computations always represent the same value as
the computations they replace. It is complete (i.e., optimal), if the program it
produces requires on every path at most as many computations as any other
program resulting from a sound PRE-transformation.