Vorbedingung (Informatik)
aus Wikipedia, der freien Enzyklopädie
Dies ist die aktuelle Version dieser Seite, zuletzt bearbeitet am 18. Oktober 2013 um 08:13 Uhr durch imported>DerHexer(127709) (Änderungen von 79.222.217.246 (Diskussion) auf die letzte Version von DerHexer zurückgesetzt (HG)).
Die Vorbedingung einer Funktion oder eines Programms gibt an, unter welchen Voraussetzungen das Verhalten der Funktion definiert ist. Die Vorbedingung ist Teil der formalen Spezifikation der Funktion (bzw. des Programms) und dient der Verifikation: Wenn sie gilt, so müssen nach Ausführung der Funktion alle Nachbedingungen erfüllt sein, sonst ist das Programm nicht korrekt.
Das Konzept von Vor- und Nachbedingungen wird vor allem in der formalen Semantik benutzt: es stellt die Basis der axiomatischen Semantik dar. Das Ziel ist es dabei, aus den Vor- und Nachbedingungen der einzelnen Teile des Programms logisch die gewünschte Nachbedingung für das gesamte Programm zu folgern.
