imported>Fan-vom-Wiki: {{Belege fehlen}}

2024-04-26T00:22:41Z

Neue Seite

{{Belege fehlen}}
Die '''Nachbedingungen''' einer [[Funktion (Informatik)|Funktion]] oder eines [[Computerprogramm|Programms]] geben an, welche [[Logische Aussage|Aussagen]] nach der Ausführung gelten müssen, falls zuvor die [[Vorbedingung (Informatik)|Vorbedingung]]en erfüllt waren. Die Nachbedingung ist Teil der [[Formale Spezifikation|formalen Spezifikation]] der Funktion (bzw. des Programms) und dient der [[Verifikation]]: Wenn die Vorbedingung gilt, so müssen nach Ausführung der Funktion alle Nachbedingungen erfüllt sein, sonst ist das Programm nicht [[Korrektheit (Informatik)|korrekt]].

Das Konzept von Vor- und Nachbedingungen wird vor allem in der [[Formale Semantik|formalen Semantik]] benutzt: es stellt die Basis der [[Axiomatische Semantik|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 [[Schlussfolgerung|folgern]].

Auch bei dem weniger formalen ''Testen'' von Software spielen Nachbedingungen eine wesentliche Rolle, da das Ergebnis von Testläufen leicht mit den Nachbedingungen verglichen werden kann. Das wird vor allem für den so genannten [[Unit-Test]] verwendet.

== Siehe auch ==
* [[Assertion (Informatik)|Assertion]]

[[Kategorie:Programmiersprachelement]]
[[Kategorie:Theoretische Informatik]]

Nachbedingung (Informatik) - Versionsgeschichte

imported>Fan-vom-Wiki: {{Belege fehlen}}