Search

In this chapter we introduce the theoretical foundations of transformational programming together with a variety of simple transformation rules. In the following chapters, these will be considered as a basis for deriving and proving correct further, more advanced, compact rules. Additionally, we will also show that these basic rules together with elementary strategies are already sufficient to do transformational program development for certain specific tasks. The examples will start from formal specifications as developed in Sect. 3.6.

In the previous chapters, it has been mentioned several times that the major part of any program development by transformations can be done at the level of applicative formulations. Nevertheless, when aiming at the efficient running of programs on conventional von Neumann machines, a few more transformations have to be available for introducing variables (the key concept of the von Neumann machine) together with related constructs such as assignment, iteration, and loops. In contrast to the transformations dealt with in earlier sections, these rules are of a much more mechanical nature. One can thus imagine that they might be performed automatically, for example by a suitable optimizing compiler. Since the whole subject, sometimes called ‘optimizing transformations’, is extensively treated in standard textbooks on compiler construction and also in [Bauer, Wossner 82] or [Illsley 88], our treatment here will be a little sketchy and by no means comprehensive. Still, it suffices to give at least a rough impression of what these rules are about.