Unter Korrektheit versteht man in der Informatik die Eigenschaft eines Computerprogramms, einer Spezifikation zu genügen (siehe auch Verifikation). Spezialgebiete der Informatik, die sich mit dieser Eigenschaft befassen, sind die Formale Semantik und die Berechenbarkeitstheorie.

Nicht abgedeckt vom Begriff Korrektheit ist, ob die Spezifikation die vom Programm zu lösende Aufgabe korrekt beschreibt (siehe dazu Validierung).

Ein Programmcode wird bezüglich einer Vorbedingung P und der Nachbedingung Q partiell korrekt genannt, wenn bei einer Eingabe, die die Vorbedingung P erfüllt, jedes Ergebnis die Nachbedingung Q erfüllt. Dabei ist es noch möglich, dass das Programm nicht für jede Eingabe ein Ergebnis liefert, also nicht terminiert.

Ein Code wird total korrekt genannt, wenn er partiell korrekt ist und zusätzlich für jede Eingabe, die die Vorbedingung P erfüllt, terminiert. Aus der Definition folgt sofort, dass total korrekte Programme auch immer partiell korrekt sind.

Der Nachweis partieller Korrektheit (Verifikation) kann mit dem wp-Kalkül erfolgen. Um zu zeigen, dass ein Programm total korrekt ist, muss hier der Beweis der Terminierung in einem gesonderten Schritt behandelt werden. Mit dem Hoare-Kalkül kann die totale Korrektheit in vielen Fällen nachgewiesen werden.

Der Nachweis der Korrektheit eines Programms kann jedoch nicht in allen Fällen geführt werden: das folgt aus dem Halteproblem bzw. aus dem Gödelschen Unvollständigkeitssatz. Die Korrektheit von Programmen zählt damit zu den nicht-berechenbaren Problemen.

Correctness

Theoretische Informatik