Korrektheit

korrekt-heit lat.-deu. Wrtdtng:: wrtl. an sich 'Gerechtheit, Gerichtetheit', gemeint ist meist Genauigkeit oder Richtigkeit wie auch Geregeltheit, wie als Geregtheit übersetzbar.

Korrektheit f.‘Richtigkeit, Fehlerlosigkeit, einwandfreies Benehmen’ (um 1800).

Korrektheit (Logik)

Korrektheit (englisch soundness) ist eine wichtige Eigenschaft formaler Systeme oder Kalküle und betrifft den Zusammenhang zwischen Syntax und Semantik, der umgangssprachlich lautet: Was formal ableitbar ist, ist auch wahr, soweit die Prämissen der Ableitung wahr sind.

In der formalen Logik wird Ableitbarkeit durch den syntaktischen Ableitungsoperator ⊢ und Schlussfolgern durch die semantische Folgerungsrelation ⊨ ausgedrückt: Ein Kalkül heißt korrekt, wenn für Aussagenmengen 𝚺 und 𝚿 aus stets 𝚺 ⊨ 𝚿 folgt. Die Semantik des Schließens wird modelltheoretisch definiert: 𝚺 ⊨ 𝚿 gilt genau dann, wenn jedes Modell von 𝚺 auch Modell von 𝚿 ist. Für die Korrektheit eines Kalküls ist hinreichend, wenn jede einzelne Ableitungsregel gültig ist. In einem korrekten Kalkül, welcher zusätzlich ein gewähltes Modell richtig beschreibt, lässt sich keine Formel herleiten, die im gewählten Modell nicht wahr ist. Allerdings hilft ein korrekter Kalkül nicht weiter, wenn er das Modell durch Axiome falsch beschreibt (z. B. postuliere 𝚺 für einen Kalkül der natürlichen Zahlen, dass die Null einen Vorgänger hat) oder inkonsistent ist (z. B. postuliere 𝚺 für einen Kalkül der natürlichen Zahlen, dass die Null einen Vorgänger hat und keinen Vorgänger hat). Aus einem solchen korrekten Kalkül lassen sich Formeln herleiten, die im gewählten Modell nicht wahr sind.

Das Gegenstück zur Korrektheit ist die Vollständigkeit eines formalen Systems. Sie besagt: Was semantisch richtig ist, lässt sich auch ableiten. Vollständigkeitssätze sind meist weitaus schwieriger zu beweisen als Korrektheitssätze; so bereitet der Beweis für die Korrektheit des Sequenzenkalküls der Prädikatenlogik keine Probleme, wohingegen der Vollständigkeitssatz schwieriger ist.

Sh ach

• Allgemeingültigkeit
• Gültigkeit
• Fehlschluss
• Korrektheit (Informatik)

Qlln

• Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Einführung in die mathematische Logik, 5. Aufl., Spektrum Akademischer Verlag; 2007, ISBN 978-3827416919
• Hans-Peter Tuschik, Helmut Wolter: Mathematische Logik – kurzgefasst. Grundlagen, Modelltheorie, Entscheidbarkeit, Mengenlehre, BI-Wiss. Verlag, Mannheim-Leipzig-Wien-Zürich 1994, ISBN 3-411-16731-9.

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 Semantikund 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 einer 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 für jede Eingabe 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ü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 der Nicht-Entscheidbarkeit des Halteproblems 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.

Sh ach

• Korrektheit (Logik)

Wblnks

• Gemeinsame Kriterien für die Prüfung und Bewertung der Sicherheit von Informationstechnik
• IT-Sicherheitskriterien und Evaluierung nach ITSEC
• Deutsche IT-Sicherheitskriterien