Next: Refal
Up: Verification via Supercompilation
Previous: Verification via Supercompilation
The supercompilation (from supervised compilation) is a
powerful semantic based program transformation technique[26,28] having a long
history well back to the 1960-70s, when it was proposed by V.
Turchin. The main idea is to observe the behaviour of a
functional program running on (partially defined) input with the aim
to define a program, which would be equivalent to the original one (on
the domain of latter), but having improved properties. The result may
be a specialized version of the original program, taking into account
the properties of known arguments, or just a re-formulated, and
sometimes more efficient equivalent program.
The transformation itself takes into account deep semantic properties of
the program. The resulting program is build
as the result of meta-interpretation,
so the syntax of the
original program is thrown away, and the
the resulting transformed program may have nothing
common in syntax with original one. As to the semantics, resulting program may
have wider domain than the source program, but both are
equivalent on the domain of the source.
This distinguishes it from other
popular techniques, such as partial evaluation [].
From the very beginning the
development of supercompilation has been conducted mainly in the
context of the Refal
programming language [27]. A few supercompilers
for Refal
were implemented with the most advanced being SCP4 [21].
SCP4 unfolds a potentially infinite tree of all
possible computations of a program with a parameterized entry point (partially
defined input). In the process, it
reduces the redundancy that could be present in the original program.
It folds the tree into a finite graph of states and transformations
between possible configurations of the computing system. And, finally,
it analyses global properties of the graph, specializes this graph
with respect to these properties and, based on the graph, constructs the
resulting program.
The resulting definition is constructed solely based on the
meta-interpretation of the source program rather than by a
step-by-step transformation of the program. For more details see
[21,19].
Next: Refal
Up: Verification via Supercompilation
Previous: Verification via Supercompilation
Alexei Lisitsa
2005-07-14