ERCIM News No.36 - January 1999

MAP: a Tool for Program Derivation based on Transformation Rules and Strategies

by Alberto Pettorossi, Maurizio Proietti, and Sophie Renault

---

Since 1987 the Department of Informatics of the University of Rome Tor Vergata and the IASI Institute of the National Research Council (CNR), Rome, have been cooperating on the development of techniques and tools for automatic program derivation and validation. This work has used a transformation methodology based on the so-called ‘rules + strategies’ approach.

The basic idea for this approach goes back to the seminal papers by Burstall-Darlington in 1977 (for the case of functional programs) and Tamaki-Sato in 1984 (for the case of logic programs). These papers show how a given specification, written as a set of recursive equations or a set of Horn clauses, can be transformed into an efficient program by applying suitable transformation rules which are guaranteed to preserve the intended semantics. The application of these rules should be guided by suitable strategies that, for some classes of initial specifications, allow us to derive efficient programs.

We are currently developing a tool, called MAP, to support the interactive derivation of logic programs by means of transformation rules and strategies. The MAP system has been implemented in SICStus Prolog and its graphical user interface has been developed using Tcl/Tk.

At present the MAP system provides a menu with a set of predefined transformation rules which include: definition introduction, definition elimination, unfolding, folding, goal replacement, generalization, and case split. If suitable conditions are satisfied, these rules preserve the least Herbrand model semantics.

In MAP the programmer also has a menu with a set of predefined strategies, ie, sequences of applications of transformation rules. Strategies are needed to derive programs with specific syntactic properties, such as: tail recursion, linear recursion, absence of existential variables and unnecessary data structures and absence of redundant nondeterminism. These syntactic properties make the derived programs very efficient in time and space.

The program derivation process requires some theorem proving capabilities. In particular, in order to apply the goal replacement rule we need to show the equivalence between a new goal and one to be replaced. For instance, during program derivation we may need to use the associativity of list concatenation, which is expressed by the goal equivalence:

Formulas of this type can be proved off-line and all equivalences can be stored in theories which represent our knowledge about the predicates used. The MAP system allows the programmer to create, load, update, and store theories which may be useful for the derivations at hand.

MAP keeps track of the history of the program derivations, and provides the user with some facilities for backtracking to previous programs and exploring alternative derivations. In MAP, program derivations can be operated on by, for instance, loading, editing, printing and saving them, and programs, theories, and histories can be restored.

We are planning several enhancements to the current system. We would like to improve the ease of interaction with the user by providing more powerful graphical tools for navigating through the tree of alternative program derivations. We would also like to be able to extract program derivations and to reuse them for deriving in a (semi-) automatic way new programs from similar initial specifications.

We are currently working to extend the system to other languages, and in particular, to: general logic programs with negation, constraint logic programs, and functional programs. We are developing libraries which allow the user to load several sets of predefined rules, strategies, and theories into the system. We also plan to design languages that enable the users to define their own rules and strategies, so that the system may work as a generic, programmable program transformer.

In addition, we intend to include modules to support automated theorem proving and program analysis. The future MAP system should be able to exploit the information produced by these modules for performing very powerful program transformations whose applicability conditions may depend on the specific properties of the programs at hand.

As already indicated in the literature, there are various applications of program transformation within the field of machine-supported software production, reuse, and validation for which the MAP system could be a useful supporting tool. Among these applications, we should like to mention program specialization, program synthesis, and program verification.

Our research is currently supported by the Italian Ministry for the Universities and Scientific and Technological Research and by CNR. More information is available at:
http://www.iasi.rm.cnr.it/~{adp,proietti}

Please contact:

Alberto Pettorossi - University of Rome - Tor Vergata,
Maurizio Proietti - IASI-CNR
Tel: +39 06 7716426
E-mail: {adp,proietti}@iasi.rm.cnr.it

Sophie Renault - Université de Montréal
E-mail: renault@IRO.UMontreal.ca