Korrektheit (Informatik) - LinkFang.de





Korrektheit (Informatik)


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 z. B. 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. Auch wenn die Korrektheit für Programme, die bestimmten Einschränkungen unterliegen, bewiesen werden kann, so zählt die Korrektheit von Programmen allgemein zu den nicht-berechenbaren Problemen.

Die Durchführung einer Überprüfung auf Korrektheit bezeichnet man als Beweis. Dabei ist ein Beweis der totalen Korrektheit ein Spezialfall eines mathematischen Beweises, erlaubt also im Gegensatz zum umgangssprachlichen Beweisbegriff eine absolute Aussage.

Weblinks


Kategorien: Theoretische Informatik

Quelle: Wikipedia - http://de.wikipedia.org/wiki/Korrektheit (Informatik) (Vollständige Liste der Autoren des Textes [Versionsgeschichte])    Lizenz: CC-by-sa-3.0

Änderungen: Alle Bilder mit den meisten Bildunterschriften wurden entfernt. Ebenso alle zu nicht-existierenden Artikeln/Kategorien gehenden internen Wikipedia-Links (Bsp. Portal-Links, Redlinks, Bearbeiten-Links). Entfernung von Navigationsframes, Geo & Normdaten, Mediadateien, gesprochene Versionen, z.T. ID&Class-Namen, Style von Div-Containern, Metadaten, Vorlagen, wie lesenwerte Artikel. Ansonsten sind keine Inhaltsänderungen vorgenommen worden. Weiterhin kann es durch die maschinelle Bearbeitung des Inhalts zu Fehlern gerade in der Darstellung kommen. Darum würden wir jeden Besucher unserer Seite darum bitten uns diese Fehler über den Support mittels einer Nachricht mit Link zu melden. Vielen Dank!

Stand der Informationen: August 201& - Wichtiger Hinweis: Da die Inhalte maschinell von Wikipedia übernommen wurden, ist eine manuelle Überprüfung nicht möglich. Somit garantiert LinkFang.de nicht die Richtigkeit und Aktualität der übernommenen Inhalte. Sollten die Informationen mittlerweile fehlerhaft sein, bitten wir Sie darum uns per Support oder E-Mail zu kontaktieren. Wir werden uns dann innerhalb von spätestens 10 Tagen um Ihr Anliegen kümmern. Auch ohne Anliegen erfolgt mindestens alle drei Monate ein Update der gesamten Inhalte.