Program Derivation
Program-Transformation.Org: The Program Transformation Wiki
Program derivation is a kind of ProgramTransformation in which an (efficient) implementation is derived from a (high-level) specification.
If the specification can be proven correct easily and the derivation preserves this correctness, it follows that the resulting implementation is correct.
Therefore, derivation is especially useful if the correctness of the final product is important and the problem it solves is very complex.
See also