php-deluxe.net - description Program derivation

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 mathematical proof that it conforms to a given program specification. The main problems with this are that

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.

=See also=

Formal verification

Hoare logic

=References=

Edsger Dijkstra, Wim H. J. Feijen, A Method of Programming , Addison-Wesley, 1988, 188 pages

Edward Cohen, Programming in the 1990 s , Springer-Verlag, 1990

Anne Kaldewaij, Programming: The Derivation of Algorithms , Prentice-Hall, 1990, 216 pages

David Gries, The Science of Programming , Springer-Verlag, 1981, 350 pages

A.J.M. van Gasteren. On the Shape of Mathematical Arguments . Lecture Notes in Computer Science #445, Springer-Verlag, 1990. Teaches how to write proofs with clarity and precision.