Correctness
Encyclopedia
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).
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.
For example, successively searching through integer
s 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. It can only show partial correctness and has to be augmented with a separate termination proof.
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
, correctness of an algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
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).
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
Halting problem
In computability theory, the halting problem can be stated as follows: Given a description of a computer program, decide whether the program finishes running or continues to run forever...
, a total correctness assertion may lie much deeper. A termination proof is a type of mathematical proof
Mathematical proof
In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...
that plays a critical role in formal verification
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
because total correctness of an algorithm depends on termination.
For example, successively searching through integer
Integer
The integers are formed by the natural numbers together with the negatives of the non-zero natural numbers .They are known as Positive and Negative Integers respectively...
s 1, 2, 3, … to see if we can find an example of some phenomenon — say an odd perfect number
Perfect number
In number theory, a perfect number is a positive integer that is equal to the sum of its proper positive divisors, that is, the sum of its positive divisors excluding the number itself . Equivalently, a perfect number is a number that is half the sum of all of its positive divisors i.e...
— 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
Number theory
Number theory is a branch of pure mathematics devoted primarily to the study of the integers. Number theorists study prime numbers as well...
.
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
Computer memory
In computing, memory refers to the physical devices used to store programs or data on a temporary or permanent basis for use in a computer or other digital electronic device. The term primary memory is used for the information in physical systems which are fast In computing, memory refers to the...
.
A deep result in proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, the Curry-Howard correspondence, states that a proof of functional correctness in constructive logic corresponds to a certain program in the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
. Converting a proof in this way is called program extraction.
Hoare logic
Hoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
is a specific formal system
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
for reasoning rigorously about the correctness of computer programs. It can only show partial correctness and has to be augmented with a separate termination proof.
See also
- Formal verificationFormal verificationIn the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
- Design by contractDesign by contractDesign by contract , also known as programming by contract and design-by-contract programming, is an approach to designing computer software...
- Program analysis (computer science)Program analysis (computer science)In computer science, program analysis is the process of automatically analysing the behavior of computer programs. Two main approaches in program analysis are static program analysis and dynamic program analysis...
- Model checkingModel checkingIn computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
- Compiler correctnessCompiler correctnessIn computing, compiler correctness is the branch of software engineering that deals with trying to show that a compiler behaves according to its language specification...