Automatic Program Derivation by Transformation

by Alberto Pettorossi and Maurizio Proietti

Over the last ten years or so the Department of Informatics of the University of Rome - Tor Vergata and the IASI Institute of CNR, Rome, have been cooperating on the development of techniques and tools for the automatic derivation of logic and functional programs using trans-formation methodology. This collaboration has also involved researchers from the Centre for Advanced Programming Methodologies, funded by Finsiel S.p.a. and the Engineering Faculty of the University of Rome - Tor Vergata. Various sets of transformation rules and strategies have been proposed for the automatic derivation of correct and efficient programs from their formal specifications. A prototype program transformer is under development.

Our research on program development by transformation is based on the so called rules + strategies approach, originally proposed in the early seventies by Burstall and Darlington. This approach was first considered in the field of logic programming by Tamaki and Sato in 1984.

In the rules + strategies approach the task of writing a correct and efficient program is realized in two phases where the first consists in writing an initial, maybe inefficient, program whose correctness can easily be shown, and the second consists in transforming the initial program in order to derive a new, more efficient version.

The separation of the issue of correctness from that of efficiency is one of the major advantages of the transformation methodology. Indeed, this methodology makes it possible to eliminate some of the difficulties encountered when applying other program development techniques. In particular, the design of intricate invariant assertions, such as those required when deriving programs by stepwise refinements, can be avoided. Program transformation has also the advantage of being adaptable to imperative and concurrent languages, as well as to functional and logic ones.

The basic idea underlying the program transformation approach can be described as follows: from an initial program P0, which can also be viewed as the initial specification, we want to obtain a final program Pn with the same semantic value, that is, we want that Sem[P0]=Sem[Pn] for some given semantic function Sem. Program Pn is often derived in several steps by constructing a sequence P0,...,Pn of programs such that for 0 < i < n , Sem[Pi]=Sem[Pi+1] , where Pi+1 is obtained from Pi by applying a transformation rule.

During the program transformation process, an attempt is made to reduce the complexity of the derived programs w.r.t. the initial ones. For this scope, we introduce so-called transformation strategies, ie meta-rules which prescribe suitable sequences of applications of the transformation rules.

At present our research is mainly focused on logic program transformation and is being carried out along the following two lines.

1. There is a considerable theoretical activity concerning the formalization and the study of the properties of transformation rules. The main objective of this study is to prove that a given set of rules preserves certain semantics of logic programs. We thus propose powerful proof methods, which are parametric with respect to the semantics under consideration. We also use advanced program analysis techniques, such as those based on abstract interpretation and termination properties.

2. To improve the efficiency of the derived programs, the transformation rules are combined into complex strategies in order to automatically improve the performance of the initial programs. These transformation strategies can be used to achieve the following objectives:

• removal of recursion in favour of iteration
• elimination of intermediate data structures
• avoidance of multiple visits of data structures
• avoidance of redundant or repeated computations
• reduction of nondeterminism
• specialization of programs to specific classes of input values.

We are currently studying the power of the proposed strategies. In particular, we analyse their termination properties w.r.t. suitable classes of initial programs and their completeness, which should be understood in the following sense: given a set of transformation rules and a syntactic property ø of the programs (eg tail-recursive or linear recursive programs), a strategy S is complete iff for any initial program P , if we are able to derive a program satisfying ¡ by using the given transformation rules in a suitable way, then we are also able to derive a program satisfying ø by using the strategy S. Recently, we have been able to show the completeness of a strategy for eliminating all unnecessary variables in logic programs, thus providing a general and powerful method for automatic program improvement.

The transformation approach to program derivation can be very effective: we are able to derive logarithmic-time programs from exponential-time programs and also to drastically improve memory utilization, so as to avoid garbage collection or the use of stacks in favour of arrays.

In our research activities we will continue to study the properties of the rules and the strategies for the transformation of logic programs, and we will also work on the development of a semi-automatic tool to support the many transformation techniques proposed so far. This tool should support activities related to program transformation, such as the definition of transformation rules, strategies, and possibly, meta-strategies, ie combinations of transformation strategies. It should also incorporate other tools for analyzing program properties via static analysis, and for measuring program performance.

During this research we have been in contact with various research centres, and in particular, with CWI (Amsterdam, Netherlands), the Catholic University of Leuven (Belgium), and the University of Pisa (Italy). From 1992 through 1995, our research project was financially supported by the Esprit Project 'Compulog II' of the European Community and the 'Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo' of CNR, Italy.

Please contact:
Alberto Pettorossi - Universitá di Roma Tor Vergata
E-mail: adp@iasi.rm.cnr.it
or Maurizio Proietti - IASI-CNR
Tel: +39 6 7716426
Email: proietti@iasi.rm.cnr.it