Program transformation
A Program Transformation is any operation which takes a program and generates a semantically equivalent program.
A generalisation of semantic equivalence is the notion of 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.
The FermaT Transformation System contains implementations for many program transformations.