Korrektheit (Informatik)
UnterKorrektheitversteht man in derInformatikdie Eigenschaft einesComputerprogramms,einerSpezifikationzu genügen (siehe auchVerifikation). Spezialgebiete der Informatik, die sich mit dieser Eigenschaft befassen, sind dieFormale Semantikund dieBerechenbarkeitstheorie.
Nicht abgedeckt vom BegriffKorrektheitist, ob dieSpezifikationdie vom Programm zu lösende Aufgabe korrekt beschreibt (siehe dazuValidierung).
Ein Programmcode wird bezüglich einerVorbedingungP und einerNachbedingungQpartiell korrektgenannt, 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 für jede Eingabeterminiert.
Ein Code wirdtotal korrektgenannt, 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 z. B. mit demwp-Kalkülerfolgen. Um zu zeigen, dass ein Programm total korrekt ist, muss hier der Beweis der Terminierung in einem gesonderten Schritt behandelt werden. Mit demHoare-Kalkülkann 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 derNicht-EntscheidbarkeitdesHalteproblemsbzw. aus demGödelschen Unvollständigkeitssatz.Auch wenn die Korrektheit für Programme, die bestimmten Einschränkungen unterliegen, bewiesen werden kann, so zählt die Korrektheit von Programmen allgemein zu dennicht-berechenbarenProblemen.
Die Durchführung einer Überprüfung auf Korrektheit bezeichnet man als Beweis. Dabei ist ein Beweis der totalen Korrektheit ein Spezialfall einesmathematischen Beweises,erlaubt also im Gegensatz zum umgangssprachlichen Beweisbegriff eine absolute Aussage.