next up previous
Next: Refal Up: Verification via Supercompilation Previous: Verification via Supercompilation

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 up previous
Next: Refal Up: Verification via Supercompilation Previous: Verification via Supercompilation
Alexei Lisitsa 2005-07-14