Correctness (computer science)
In theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is functional correctness, which refers to the input-output behavior of the algorithm (i.e., for each input it produces an output satisfying the specification). A deep result in proof theory, the Curry–Howard correspondence, states that a proof of functional correctness in constructive logic corresponds to a certain program in the lambda calculus. Converting a proof in this way is called program extraction.
- Comment
- enIn theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is functional correctness, which refers to the input-output behavior of the algorithm (i.e., for each input it produces an output satisfying the specification). A deep result in proof theory, the Curry–Howard correspondence, states that a proof of functional correctness in constructive logic corresponds to a certain program in the lambda calculus. Converting a proof in this way is called program extraction.
- Has abstract
- enIn theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is functional correctness, which refers to the input-output behavior of the algorithm (i.e., for each input it produces an output satisfying the specification). Within the latter notion, partial correctness, requiring that if an answer is returned it will be correct, is distinguished from total correctness, which additionally requires that an answer is eventually returned, i.e. the algorithm terminates. Correspondingly, to prove a program's total correctness, it is sufficient to prove its partial correctness, and its termination. The latter kind of proof (termination proof) can never be fully automated, since the halting problem is undecidable. For example, successively searching through integers 1, 2, 3, … to see if we can find an example of some phenomenon—say an odd perfect number—it is quite easy to write a partially correct program (see box). But to say this program is totally correct would be to assert something currently not known in number theory. A proof would have to be a mathematical proof, assuming both the algorithm and specification are given formally. In particular it is not expected to be a correctness assertion for a given program implementing the algorithm on a given machine. That would involve such considerations as limitations on computer memory. A deep result in proof theory, the Curry–Howard correspondence, states that a proof of functional correctness in constructive logic corresponds to a certain program in the lambda calculus. Converting a proof in this way is called program extraction. Hoare logic is a specific formal system for reasoning rigorously about the correctness of computer programs. It uses axiomatic techniques to define programming language semantics and argue about the correctness of programs through assertions known as Hoare triples. Software testing is any activity aimed at evaluating an attribute or capability of a program or system and determining that it meets its required results. Although crucial to software quality and widely deployed by programmers and testers, software testing still remains an art, due to limited understanding of the principles of software. The difficulty in software testing stems from the complexity of software: we can not completely test a program with moderate complexity. Testing is more than just debugging. The purpose of testing can be quality assurance, verification and validation, or reliability estimation. Testing can be used as a generic metric as well. Correctness testing and reliability testing are two major areas of testing. Software testing is a trade-off between budget, time and quality.
- Is primary topic of
- Correctness (computer science)
- Label
- enCorrectness (computer science)
- Link from a Wikipage to an external page
- books.google.com/books%3Fid=6YAXDQAAQBAJ&printsec=frontcover%23v=onepage&q=correctness&f=false
- books.google.com/books%3Fid=l5FZxDY3yi0C&printsec=frontcover%23v=onepage&q=correctness&f=false
- www.coopertoons.com/education/haltingproblem/haltingproblem.html
- stanford.library.sydney.edu.au/entries/computer-science/
- Link from a Wikipage to another Wikipage
- Algorithm
- C (programming language)
- Category:Formal methods terminology
- Category:Software quality
- Category:Theoretical computer science
- Compiler correctness
- Computer memory
- Constructive logic
- Curry–Howard correspondence
- Deep result
- Design by contract
- Formal system
- Formal verification
- Halting problem
- Hoare logic
- Integer
- Lambda calculus
- Mathematical proof
- Model checking
- Number theory
- Perfect number
- Program analysis
- Program derivation
- Program specification
- Proof theory
- Software testing
- Termination proof
- Theoretical computer science
- Undecidable problem
- SameAs
- 3KzRT
- Correction d'un algorithme
- Correctitud
- Correctness (computer science)
- Corretude (lógica)
- Helyesség (számítástechnika)
- Korrektheit (Informatik)
- m.01 0xk
- Poprawność całkowita
- Q360812
- صحت (علوم رایانه)
- 正当性 (計算機科学)
- 正确性 (计算机科学)
- Subject
- Category:Formal methods terminology
- Category:Software quality
- Category:Theoretical computer science
- WasDerivedFrom
- Correctness (computer science)?oldid=1052944498&ns=0
- WikiPageLength
- 6698
- Wikipage page ID
- 357339
- Wikipage revision ID
- 1052944498
- WikiPageUsesTemplate
- Template:Reflist
- Template:Short description
- Template:Software quality
- Template:Use dmy dates