In
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, 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
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
is to first write a program, and then provide a
proof that it conforms to a given
specification
A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard.
There are different types of technical or engineering specificati ...
. 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 shorter, 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.
The
Bird-Meertens Formalism is an approach to program derivation.
See also
*
Automatic programming
In computer science, the term automatic programming identifies a type of computer programming in which some mechanism generates a computer program to allow human programmers to write the code at a higher abstraction level.
There has been little ...
*
Hoare logic
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and log ...
*
Program refinement
*
Design by contract
*
Program synthesis In computer science, program synthesis is the task to construct a program that provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both fields ...
*
Proof-carrying code Proof-carrying code (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application's executable code. The host system can quickly verify the validity of the proo ...
References
*
Edsger W. 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
*
Carroll Morgan (computer scientist)
Charles ''Carroll'' Morgan (born 1952) is an American computer scientist who moved to Australia in his early teens. He completed his education there (high school, university, several years in industry), including a Doctor of Philosophy (Ph.D.) ...
''Programming from Specifications'' International Series in Computer Science (2nd ed.), Prentice-Hall, 1998.
*
Eric C.R. Hehner''a Practical Theory of Programming'' 2008, 235 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.
* Martin Rem. "Small Programming Exercises", appeared in ''Science of Computer Programming'', Vol.3 (1983) through Vol.14 (1990).
* Roland Backhouse. ''Program Construction: Calculating Implementations from Specifications''. Wiley, 2003. .
* Derrick G. Kourie, Bruce W. Watson. ''The Correctness-by-Construction Approach to Programming''. Springer-Verlag, 2012. {{ISBN, 978-3-642-27919-5. Provides a step-by-step explanation of how to derive mathematically correct algorithms using small and tractable refinements.