Korrektheit (Informatik)

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.

Siehe auch

Weblinks


Wikimedia Foundation.

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Korrektheit — Das mathematische Attribut Korrektheit (von korrekt = richtig) bezeichnet: in der mathematischen Logik eine Eigenschaft mancher formaler Systeme oder Kalküle, siehe Korrektheit (Logik). in der Softwaretechnik eine Eigenschaft eines… …   Deutsch Wikipedia

  • Test (Informatik) — Ein Softwaretest ist ein Test während der Softwareentwicklung, um die Funktionalität einer Software an den Anforderungen und ihre Qualität zu messen, und Softwarefehler zu ermitteln. Inhaltsverzeichnis 1 Definition 2 Ziele 3 Testplanung …   Deutsch Wikipedia

  • Partielle Korrektheit — 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 …   Deutsch Wikipedia

  • Totale Korrektheit — 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 …   Deutsch Wikipedia

  • MPI Informatik — Max Planck Institut für Informatik Sitz in Saarbrücken Kategorie: Forschungseinrichtung Träger: Max Planck Gesellschaft Rechtsform des Trägers: Eingetragener Verein …   Deutsch Wikipedia

  • Max-Planck-Institut für Informatik — Max Planck Institut Informatik Sitz in Saarbrücken Kategorie: Forschungseinrichtung Träger: Max Planck Gesellschaft Rechtsform des Trägers …   Deutsch Wikipedia

  • Validierung (Informatik) — Validierung in der Informatik und Softwaretechnik ist die dokumentierte Beweisführung, dass ein System die Anforderungen in der Praxis erfüllt. Inhaltsverzeichnis 1 Validierung als Plausibilitätsprüfung 2 Einsatzgebiete 3 Validierung in der… …   Deutsch Wikipedia

  • Assertion (Informatik) — Eine Zusicherung oder Assertion (lat./engl. für Aussage; Behauptung) ist eine Aussage über den Zustand eines Computer Programms oder einer elektronischen Schaltung. Mit Hilfe von Zusicherungen können logische Fehler im Programm oder Defekte in… …   Deutsch Wikipedia

  • Invarianz (Informatik) — In der objektorientierten Programmierung bedeutet Kovarianz und Kontravarianz, ob ein Aspekt gleichartig der Vererbungsrichtung (kovariant) oder entgegengesetzt zu dieser (kontravariant) ist. Liegt in der Unterklasse keine Änderung gegenüber der… …   Deutsch Wikipedia

  • Kontravarianz (Informatik) — In der objektorientierten Programmierung bedeutet Kovarianz und Kontravarianz, ob ein Aspekt gleichartig der Vererbungsrichtung (kovariant) oder entgegengesetzt zu dieser (kontravariant) ist. Liegt in der Unterklasse keine Änderung gegenüber der… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”