Program transformation characterises a methodology of software development where one derives a program from a formal, usually functional or declarative specification by stepwise application of semantics-preserving transformation rules. The resulting program is not only correct by construction, i.e., fulfils its specification, but may also meet further important criteria such as efficiency.
A concrete result of the application of this approach to functional programming is the interactive, prototypic transformation system Ultra, which offers a good basis for further studies in the context of formal program development.