Jump to content

Program transformation

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Ruud Koot (talk | contribs) at 12:45, 29 January 2011 (cat). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

A program transformation is any operation that takes a program and generates another program. It is often important that the derived program be semantically equivalent to the original, relative to a particular formal semantics. Other program transformations may generate programs that semantically differ from the original in predictable ways.[1]

A generalisation of semantic equivalence is the notion of program refinement: one program is a refinement of another if it terminates on all the initial states for which the original program terminates, and for each such state it is guaranteed to terminate in a possible final state for the original program. In other words, a refinement of a program is more defined and more deterministic than the original program. If two programs are refinements of each other, then the programs are equivalent.[2]

While program transformations can be defined as manual procedures, it is more useful in practice to use a program transformation system (such as Stratego/XT, TXL, DMS, ASF+SDF or Fermat), a tool that can accept and apply specifications of program transformations. Program transformations may be specified as automated procedures that modify compiler data structures (e.g. abstract syntax trees) representing the program text, or may be specified more conveniently using patterns representing parameterized source code text fragments.

A practical requirement for program transformation systems is that they be able to process the source code for the programming language of the application system to be transformed. For instance, transforming C++ is a notoriously hard problem. For a program transformation system to be used in a wide variety of circumstances, it must be able to handle a wide variety of languages. This requires the program transformation system to have a robust parsing technology (YACC is not adequate; most popular languages do not have LALR(1) grammars), a significant investment in building the language front ends of interest, and supporting static analyses to verify conditions on complex transforms. The problem of building adequate front ends for languages and supporting static analyses may be of equal difficulty as building the program transformation system itself.

See also

References

  1. ^ Ward, Martin, "Proving Program Refinements and Transformations", DPhil Thesis, Oxford University, 1989
  2. ^ Ward, Martin, Papers