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. Program derivation tries to remedy these shortcomings by The Bird-Meertens Formalism is an approach to program derivation.
- Comment
- enIn 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. Program derivation tries to remedy these shortcomings by The Bird-Meertens Formalism is an approach to program derivation.
- Has abstract
- enIn 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 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.
- Hypernym
- Derivation
- Is primary topic of
- Program derivation
- Label
- enProgram derivation
- Link from a Wikipage to an external page
- www.cs.ox.ac.uk/publications/books/PfS/
- www.cs.toronto.edu/~hehner/aPToP/
- Link from a Wikipage to another Wikipage
- Automatic programming
- Bird-Meertens Formalism
- Carroll Morgan (computer scientist)
- Category:Program derivation
- Computer science
- Correctness (computer science)
- Design by contract
- Edsger W. Dijkstra
- Eric Hehner
- Formal verification
- Hoare logic
- Mathematical proof
- Program refinement
- Program specification
- Program synthesis
- Proof-carrying code
- SameAs
- 4tNqR
- m.02dy4d
- Q7248413
- プログラム導出
- Subject
- Category:Program derivation
- WasDerivedFrom
- Program derivation?oldid=873462453&ns=0
- WikiPageLength
- 3065
- Wikipage page ID
- 474691
- Wikipage revision ID
- 873462453
- WikiPageUsesTemplate
- Template:ISBN