In der Computerprogrammierung ist eine Postbedingung eine Bedingung oder Prädikat, das immer gerade nach der Ausführung von einer Abteilung des Codes oder nach einer Operation in einer formellen Spezifizierung wahr sein muss. Postbedingungen werden manchmal mit Behauptungen innerhalb des Codes selbst geprüft. Häufig werden Postbedingungen einfach in die Dokumentation der betroffenen Abteilung des Codes eingeschlossen.

Zum Beispiel: Das Ergebnis eines factorial ist immer eine ganze Zahl und größer oder gleich 1. So würde ein Programm, das den factorial einer Eingangszahl berechnet, Postbedingungen dass das Ergebnis nach der Berechnung haben, eine ganze Zahl und dass er sein, größer oder gleich 1 sein. Ein anderes Beispiel: Ein Programm, das die Quadratwurzel einer Eingangszahl berechnet, könnte die Postbedingungen dass das Ergebnis haben, eine Zahl und dass sein Quadrat sein, dem Eingang gleich sein.

Postbedingungen in der objektorientierten Programmierung

In der objektorientierten Programmierung sind Postbedingungen, zusammen mit Vorbedingungen und Klasse invariants Bestandteile des Softwarebaumethode-Designs durch den Vertrag.

Die Postbedingung für jede Routine ist eine Behauptung der Eigenschaften, die nach der Vollziehung der Ausführung der Routine versichert werden. Da es sich auf den Vertrag der Routine, die Postbedingungsangebot-Versicherung potenziellen Anrufern bezieht, dass in Fällen, die die Routine ein Staat herbeigerufen wird, in dem seine Vorbedingung hält, die durch die Postbedingung erklärten Eigenschaften gesichert werden.

Beispiel von Eiffel

Das folgende in Eiffel geschriebene Beispiel setzt den Wert eines auf einem von den Anrufern vorausgesetzt dass Argument gestützten Klassenattributes

set_hour (a_hour: GANZE ZAHL)

- Satz `Stunde' zu `a_hour'

verlangen Sie

valid_argument: 0

Postbedingungen und Erbe

In Gegenwart vom Erbe tun die Routinen, die durch Nachkomme-Klassen (Unterklassen) geerbt sind, so mit ihren Verträgen, der ihre Vorbedingungen und Postbedingungen in der Kraft ist. Das bedeutet, dass irgendwelche Durchführungen oder Wiederdefinitionen von geerbten Routinen auch geschrieben werden müssen, um ihren geerbten Vertrag zu erfüllen. Postbedingungen können in wiederdefinierten Routinen modifiziert werden, aber sie können nur gestärkt werden. D. h. die wiederdefinierte Routine kann die Vorteile vergrößern, die sie dem Kunden zur Verfügung stellt, aber jene Vorteile nicht vermindern kann.

Siehe auch

• Vorbedingung
• Design durch den Vertrag
• Logik von Hoare
• Invariants, der durch Bedingungen unterstützt ist
• Datenbankabzug