Correctness (computer science)
In computer science, correctness is understood as the property of a computer program to meet a specification (see also verification ). Special areas of computer science that deal with this property are formal semantics and computability theory .
The term correctness does not cover whether the specification correctly describes the task to be solved by the program (see also validation ).
A program code is said to be partially correct with regard to a precondition P and a postcondition Q if, in the case of an input that fulfills the precondition P, every result fulfills the postcondition Q. It is still possible that the program does not return a result for every entry, i.e. it does not terminate for every entry .
A code is called totally correct if it is partially correct and additionally terminates for every input that fulfills precondition P. From the definition it follows immediately that totally correct programs are always partially correct.
Proof of partial correctness (verification) can e.g. B. be done with the wp calculation . In order to show that a program is totally correct, the proof of the termination must be treated here in a separate step. With the Hoare calculus , total correctness can be proven in many cases.
Proof of the correctness of a program cannot be provided in all cases: This follows from the non-decidability of the halting problem or from Gödel's incompleteness theorem . Even if the correctness of programs that are subject to certain restrictions can be proven, the correctness of programs is generally one of the non-calculable problems.
Performing a correctness check is called proof. A proof of total correctness is a special case of a mathematical proof and, in contrast to the colloquial term of proof , allows an absolute statement.