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

cedural optimization is characterized by treating the procedures of a program
separatly and independently of each other. In this section, we recall the essence
of PRE for this setting under the perspective of soundness and completeness on
both the transformation and the analysis level.

3.1 Transformation Level

As recalled in Section 1, the essence of PRE is to insert at some program points
initializations of a specic temporary with the computation under consideration,
and to replace some of the original occurrences of this computation by the re-
spective temporary. Computations of dierent patterns, i.e., of lexically dierent
computations, are treated separately by this approach. 4 As usual, we will thus
develop the background of PRE for an arbitrary, but xed computation pattern
t . As a side-eect, this allows us to use a simple, unparameterized notation.

Sound PRE. Intuitively, a PRE-transformation is sound , if it does not aect the
program semantics. This requires that insertions and replacements are admissi-
ble. For insertions, this means that they are only made at safe program points.
This guarantees that there is no program path on which the computation of a
new value is introduced. In particular, no path may suer from a new run-time
error. For replacements, admissibility means that every program path reaching
a program point where an original computation has been replaced by a tempo-
rary has passed an insertion point, which is not followed by a modication of an
operand of the computation under consideration. This guarantees that wherever
a computation has been replaced by a temporary, the value of this temporary
coincides with the value produced by an evaluation of the computation.
Note that soundness as dened here is slightly more liberal as its informally
introduced counterpart of Section 1. It does not require performance preserva-
tion, i.e., it does not require that PRE-transformations must not decrease the
performance of programs. We make this distinction explicit by speaking of weak
and strong admissibility, respectively. This will be important in Section 4 and
Section 5. As usual for PRE, the performance aspect addressed by strong ad-
missibility is taken into account by the issue of completeness.

Complete PRE. While soundness of PRE in its weak sense focuses on se-
mantics preservation, completeness focuses on performance preservation and
improvement. For PRE, it is common to measure performance in terms of the
number of computations which are executed on a program path. Formally, this
leads us to the notion of computationally optimal PRE-transformations, which
are the \greatest" elements of a pre-order \computationally better" on the set
of sound PRE-transformations.
A PRE-transformation is computationally better than a PRE-transformation

T 0 if for every program the program produced by

T

T requires on every path from

4 For clarity, this is sometimes called syntactic PRE in contrast to the more ambitious
semantic PRE, which aims at eliminating partially redundant computations also
among lexically dierent, but semantically equivalent computations (cf. [25]).