Program derivation

In computer science, program derivation is the derivation of a program from its specification, by mathematical means.

To derive a program means to write a formal specification, which is usually non-executable, and then apply mathematically correct rules in order to obtain an executable program satisfying that specification. The program thus obtained is then correct by construction. Program and correctness proof are constructed together.

The approach usually taken in formal verification is to first write a program, and then provide a proof that it conforms to a given specification. The main problems with this are that

Program derivation tries to remedy these shortcomings by

Terms that are roughly synonymous with program derivation are: transformational programming, algorithmics, deductive programming.

The Bird-Meertens Formalism is an approach to program derivation.

See also

References

This article is issued from Wikipedia - version of the Sunday, October 11, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.