Transformation techniques; constructive or destructive? (Panel Session)

摘要

R.M. Burstall:

The Transformation Approach to Program Development

The postulate underlying the transformation approach to program development is that programs are complicated, hard to understand and prone to errors because we want them to be efficient. The desire for efficiency saturates our programming habits, so much so that the simplest and least efficient way to write a program never even crosses our mind. In contrast mathematicians in making definitions seek clarity and what Dijkstra calls 'separation of concerns': they pay no attention to efficiency of computation.

So the idea is to start with a program which does the right job but entirely sacrifices efficiency in favour of simplicity and modularity. We then transform it by correctness preserving transformations until a tolerably efficient, though less perspicuous, program is obtained.

E.W. Dijkstra:

Given the specifications, a text fit for "automatic execution" has to be composed, and it has to be proved that results satisfying the specifications correspond to that text. For the purpose of this discussion I regard that proof obligation as the core of the programming task.

The idea of program transformations is to produce the desired text B not directly, but to derive it from a text A via successive transformations from a suitable repertoire, the assumption being that the text A is the easier one to design, while the text B, when viewed as a program, is the more attractive one. The correctness proof for text B then consists of (a) the correctness proof for the original program A, (b) the chain of transformations with for each transformation the verification that it has been legally applied.

P. Pepper:

Our trouble comes from the - apparently intrinsic - incompatibility of clearness and efficiency which forces us to change over from the easily readable to the easily executable. This means organizing the construction of software in the form of a development process gradually abandoning clarity in favour of economy. If the single steps of this process are done according to formalized rules they are called program transformations. The discovery was that they can be done even in complicated cases.

A programming methodology should be applicable to all stages of such a development in a uniform way. Transformations can be used with existential quantifiers, recursive functions, variables and with goto's equally well; they harmonize particularly well with specification tools like abstract data types and characteristic predicates and give freedom for programming styles and notations.