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. Wikibooks has more about this subject: Wikiversity Riverside Graphics Lab Open Directory Project: Computer Science Collection of Computer Science Bibliographies Belief that title science in computer science is inappropriate Categories: Computer science | Academic disciplines ... Flowcharts are often used to represent algorithms. ... A program specification is the definition of what a computer program is expected to do. ... Program verification is the process of formally proving that a computer program does exactly what is stated in the program specification it was written to realize. ...

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. In computability theory the halting problem is a decision problem which can be informally stated as follows: Given a description of an algorithm and its initial input, determine whether the algorithm, when executed on this input, ever halts (completes). ...

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. The integers consist of the positive natural numbers (1, 2, 3, …) the negative natural numbers (−1, −2, −3, ...) and the number zero. ... In mathematics, a perfect number is an integer which is the sum of its proper positive divisors, excluding itself. ... In mathematics, the integer prime-factorization (also known as prime decomposition) problem is this: given a positive integer, write it as a product of prime numbers. ... Traditionally, number theory is that branch of pure mathematics concerned with the properties of integers. ...

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. Proof theory, studied as a branch of mathematical logic, represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. ... The Curry-Howard correspondence is the close relationship between computer programs and mathematical proofs; the correspondence is also known as the Curry-Howard isomorphism, or the formulae-as-types correspondence. ... Intuitionistic logic, or constructivist logic, is the logic used in mathematical intuitionism and other forms of mathematical constructivism. ... The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ...

See also

• Hoare logic