# 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

- ↑ Dunlop, Douglas D.; Basili, Victor R. (June 1982). "A Comparative Analysis of Functional Correctness" (PDF).
*Communications of the ACM*.**14**(2): 229–244. doi:10.1145/356876.356881. - ↑ Manna, Zohar; Pnueli, Amir (September 1974). "Axiomatic approach to total correctness of programs".
*Acta Informatica*.**3**(3): 243–263. doi:10.1007/BF00288637. - ↑ Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming" (PDF).
*Communications of the ACM*.**12**(10): 576–580. doi:10.1145/363235.363259.