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

of program analyses computing this information are commonly known as type
analysis . This is particularly challenging in the presence of additional features
like inheritance and polymorphism. While this is often considered to reflect a
flavour quite specic for object-oriented languages, it is worth noting that proce-
dure variables and formal procedures introduce similar phenomena in programs
of classical imperative languages (cf. [13]). In fact, concerning PRE, one en-
counters essentially the same problems as in the interprocedural setting. The
reusability of the as-early-as-possible placing strategy in the object-oriented set-
ting is liable to the same limitations than in the interprocedural one. We thus
do not discuss this in more detail here, but refer to [16] and [26], where this
has been sketched for a Smalltalk and an Oberon-like language, respectively,
based on specic versions of soundness and completeness theorems applying to
the respective settings considered there.

7 Discussion: Failures, Remedies, and Reuse

Reasons of Failure. Intuitively, an important reason for the missing robustness
of the as-early-as-possible placing strategy with respect to paradigm changes is
the failure of the Safety Lemma 1. In fact, this lemma does generally not carry
over to more advanced settings and paradigms. In Figure 9 this is demonstrated
for the interprocedural and the explicitly parallel setting. Each of the nodes of
procedure 2 in Figure 9(a) is safe, however, none of them is up-safe or down-

safe. Analogously, this holds for the marked node of the right component of the
explicitly parallel program shown in Figure 9(b).

c)

a) b)

π : a, b, x π

1 2

ParBegin

No computation of

c := a x := a+b

"a+b"
along this path!

y := a+b

x := a+b

π

x := a+b call

2

a := ...

Placing "a+b" is safe here!
(Though it is neither up-safe
nor down-safe!)

call π x := a+b

2

z := a+b z := c+b

Up-safe Points
Down-safe Points
Safe Points

ParEnd

Fig. 9. Failure of Safety Lemma 1 in advanced settings.

The failure of the Safety Lemma 1 in advanced settings is in fact quite typical.
As demonstrated e.g. in [25], it also fails in the intraprocedural setting when
switching from syntactic to semantic PRE. In the example of Figure 9(c) the
blackened node is safe without being up-safe or down-safe.