Program derivation

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
* the resulting proof is often long and cumbersome;
* no insight is given as to how the program was developed; it appears "like a rabbit out of a hat";
* should the program happen to be incorrect in some subtle way, the attempt to verify it is likely to be long and certain to be fruitless.

Program derivation tries to remedy these shortcomings by
* keeping proofs short, by development of appropriate mathematical notations;
* making design decisions through formal manipulation of the specification.

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

ee also

* Formal verification
* Hoare logic
* Program refinement
* Design by contract

References

* Edsger Dijkstra, Wim H. J. Feijen, "A Method of Programming", Addison-Wesley, 1988, 188 pages
* Edward Cohen, "Programming in the 1990s", 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.


Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Minimalist program — Linguistics …   Wikipedia

  • Edsger W. Dijkstra — Edsger Wybe Dijkstra Born May 11, 1930(1930 05 11) Rotterdam, Netherl …   Wikipedia

  • Maurice Clint — was professor of Computer Science at Queen s University Belfast, Northern Ireland. His research interests include parallel algorithms for numerical linear algebra and the use of formal methods in the development of parallel and distributed… …   Wikipedia

  • Euclidean geometry — A Greek mathematician performing a geometric construction with a compass, from The School of Athens by Raphael. Euclidean geometry is a mathematical system attributed to the Alexandrian Greek mathematician Euclid, which he described in his… …   Wikipedia

  • Xmonad — Infobox Software name = xmonad caption = xmonad in tiling mode author = Spencer Janssen, Don Stewart, Jason Creighton released = latest release version = 0.8 [ [http://www.haskell.org/pipermail/xmonad/2008 September/006254.html ANNOUNCE: xmonad 0 …   Wikipedia

  • Natural deduction — In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the natural way of reasoning. This contrasts with the axiomatic systems which instead use… …   Wikipedia

  • Constraint logic programming — Programming paradigms Agent oriented Automata based Component based Flow based Pipelined Concatenative Concurrent computing …   Wikipedia

  • Linguistic minimalism — Minimalism in the sense described here is not related to Minimalism, the artistic and cultural movement. Much current research in transformational grammar is inspired by Noam Chomsky s Minimalist Program . [cite book|title=The Minimalist… …   Wikipedia

  • Transformational grammar — In linguistics, a transformational grammar, or transformational generative grammar (TGG), is a generative grammar, especially of a natural language, that has been developed in a Chomskyan tradition. Additionally, transformational grammar is the… …   Wikipedia

  • science, philosophy of — Branch of philosophy that attempts to elucidate the nature of scientific inquiry observational procedures, patterns of argument, methods of representation and calculation, metaphysical presuppositions and evaluate the grounds of their validity… …   Universalium

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”