Jump to content

Program derivation

Edit links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Zoltar0 (talk | contribs) at 10:15, 18 February 2004. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Program derivation - to derive 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 you obtain is then proved correct by construction.

The approach usually taken in Formal verification is that you first write a program, and then you provide a proof that it conforms to a given 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
  • discover the program by manipulation of the specification


See also:

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
  • 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.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Program_derivation&oldid=2431676"