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 chapter we surveyed some approaches to requirements engineering in the framework of traditional software engineering. All these approaches aim at providing a formalism for precisely describing a problem to be solved. None of them, however, except for Gist, allows the formulation of a formal problem specification in the (intuitive) sense of Sect. 1.5.

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.

Applicative programs, irrespective of whether given as an initial operational problem specification or derived using the transformations and tactics dealt with so far, can often be further manipulated. In particular, modifications can be carried out that aim at increasing efficiency by speeding up the performance of certain computations, avoiding duplicated evaluations of expressions, and so on. Most of these manipulations could also be done later in the development, say on a procedural level. However, experience (see for example [Burstall, Darlington 77] and [Pepper, Partsch 80]) has shown that it is advisable to do these manipulations on the applicative level as far as possible, thus profiting from the obvious advantages (such as ‘referential transparency’ [Quine 60]) of this level of formulation. Thus, for example, all techniques that in a procedural environment are referred to as ‘loop fusion’ are covered in an applicative scenario by the much more general techniques for merging of computations (see below).