Program derivation

In computer science, program derivation is the derivation 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. The program thus obtained is then proved correct by construction.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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

Related Topics:
Formal verification - Proof - Specification

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• the resulting proof is long and cumbersome
• no insight is given as to how the program was developed; it appears "like a rabbit out of a hat"

Program derivation tries to remedy these shortcomings by

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• keeping proofs short, by development of appropriate mathematical notations
• discovering the program by manipulation of the specification

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

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

 
Program derivation: See also ►