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
