# Correctness (computer science)

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 expected output).^{[1]}

A distinction is made between **total correctness**, which additionally requires 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. A termination proof is a type of mathematical proof that plays a critical role in formal verification because total correctness of an algorithm depends on termination.^{[2]}

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 (using long division by two 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 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.^{[3]} It uses axiomatic techniques to define programming language semantics and argue about the correctness of programs through assertions known as Hoare triples.

## See also

- Formal verification
- Design by contract
- Program analysis (computer science)
- Model checking
- Compiler correctness
- Program derivation

## References

- ↑
**Lua error in Module:Citation/CS1/Identifiers at line 47: attempt to index field 'wikibase' (a nil value).** - ↑
**Lua error in Module:Citation/CS1/Identifiers at line 47: attempt to index field 'wikibase' (a nil value).** - ↑
**Lua error in Module:Citation/CS1/Identifiers at line 47: attempt to index field 'wikibase' (a nil value).**