kirancodes.me
To Proof Maintenance & Beyond!

Transformational Programming - Applications to Algorithms and Systems

Robert Paige

Abstract

Ten years ago Cheatham and Wegbreit [4] proposed a transformational program development methodology based on notions of top-down stepwise program refinement first expressed by Dijkstra [10] and Wirth [45]. A schema describing the process of this methodology is given in fig. 1. To develop a program by transformation, we first specify the program in as high a level of abstraction and as great a degree of clarity as our programming language admits. This high level problem statement program P is proved correct semimechanically according to some standard approach (see Flovd and Hoare [15, 21]), Next, using an interactive system equipped with a library of encoded transformations, each of which maps a correct program into another equivalent program, we select and apply transformations one at a time to successive versions of the program until we obtain a concrete, low level, effecient implementation version P'. The goals of transformational programming are to reduce programming labor, improve program reliability, and upgrade program performance. In order for labor to be reduced, the effort required to obtain P, prove it correct, and derive P' by transformation should be less than the effort required to code P from scratch, and also to debug it. Program reliability will be improved if P can be certified correct, and if each transformation preserves program meaning. Finally, program performance will be upgraded if transformations are directed towards increased efficiency.

Related papers