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

DFA
Specification

Intraprocedural
Interprocedural

DFA
Framework

Object-oriented
Parallel

Conditional

Effectivity
Theorem

Coincidence
Theorem

3a) 3b)

Correctness Termination

Program
Property
φ

Proof
Obligations:

2 3b)

1 3a)

Coincidence Effectivity

Equivalence

Fig. 10. The black-box view of DFA frameworks.

loosely related elds, the choice of reusability aimed at addressing a challenge
which can be considered central for computer science: mastering complexity in
software design. In fact, an inexpensive means for this is reuse of successful
approaches in new environments. Under the perspective of reusability, we inves-
tigated the benets and limitations of this approach for optimizing compilation.
Using PRE as example we demonstrated that usually the rationale guarantee-
ing the soundness and completeness of an optimization in a specic setting is
quite sensitive to setting and paradigm changes. In general, this requires setting
and paradigm-dependent adaptations in order to accommodate their specics.
However, as demonstrated by PRE this is generally worth the eort. In fact, the
example of distribution assignment placement, the combination of partially re-
dundant assignment elimination and partially dead-code elimination, shows that
optimizations are often much more powerful in a setting dierent from the one
they were originally designed for. Further research in this direction is a major
concern of future work. Progress on this issue, in particular, the intensied de-
velopment of paradigm-transcending approaches can substantially contribute to
bridging gaps between communities working (too) often on quite similar prob-
lems in dierent paradigms without utilizing synergies of their work, and hence,
to solving the overall problem: mastering complexity.

Acknowledgements. We dedicate this article to Hans Langmaack. It presents
a prole of our work on optimizing compilation under the perspective of sound-
ness and completeness, a focal point of his research interests. We appreciate his
constant encouragement and support, and gratefully acknowledge the inspiring
and stimulating impact of his advice and attitude towards computer science on
our research.