Correctness (computer science)

Under correctness is understood in computer science, the property of a computer program to satisfy a specification (see verification ). Specialized areas of computer science that deal with this property are the formal semantics and computability theory.

Not covered by the concept of correctness is whether the specification describes the problem to be solved by the program task correctly (see validation).

A program code with respect to a precondition P and the postcondition Q partially correctly called when in an entry that satisfies the precondition P, each result satisfies the postcondition Q. It is still possible that the program does not provide a result for each input, not terminated.

A code is called totally correct if it is partially correct and in addition for each input that satisfies the precondition P, terminated. From the definition it follows immediately that totally correct programs are always partially correct.

The proof of partial correctness (verification) can be done eg with the wp- calculus. To show that a program is totally correct, the proof of the termination must be treated in a separate step here. With the Hoare - calculus that total correctness can be detected in many cases.

However, the proof of correctness of a program can not be performed in all cases: this follows from the halting problem and Gödel's incompleteness theorem from the. Even if the accuracy of programs, which are subject to certain limitations, can be demonstrated, the correctness of programs is one generally non- predictable problems.

The conduct of an inspection for correctness is referred to as evidence. Here, a proof of total correctness is a special case of a mathematical proof, that allows in contrast to the colloquial notion of proof is an absolute statement.