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

Revision: r1.1 - 09 May 2001 - 21:56 - EelcoVisser
Transform > ProgramDerivation
Copyright © 1999-2020 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback