Correctness
|
|
In everyday use, the correctness of a statement is determined by whether or not it matches reality. People can think a statement is correct and be wrong. When scoring tests of knowledge where there is only one accepted answer for each problem, a device or person marks an answer as correct if it matches what the test designer has determined the testee should answer. It is common for one or more answers, thought at the time by the designer of a test to match reality, and to, at a later date, be shown to not match what can be observed, and therefore be unlikely to match reality. This often results in the mark for a testee's answer being changed from incorrect to correct at a later date. It is possible for neither the designer's, nor the testee's answer to be correct.
In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. Functional correctness refers to the input-output behaviour of the algorithm (i.e., for each input it produces the correct output). See also program verification.
A distinction is made between total correctness, where it is additionally required that the algorithm terminates, and partial correctness, which simply requires that if an answer is returned it will be correct. Since there is no general solution to the halting problem, a total correctness assertion may lie much deeper.
For example if we are successively searching though 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 (use integer factorization to check n as perfect or not). 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 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.