Nachbedingungen

Nachbedingungen sind Bedingungen, die den Zustand einer Software nach der Ausführung einer Prozedur oder Funktion beschreiben. Sie legen fest, welches Ergebnis oder welchen Zustand eine Prozedur sicher liefert, sofern sie normal beendet wird. Typisch formulieren Nachbedingungen Eigenschaften wie den Rückgabewert, Veränderungen von Feldern oder die Beziehung zwischen Eingabe und Ausgabe.

Im Kontext der vertragsbasierten Softwareentwicklung (Design by Contract) bilden Nachbedingungen zusammen mit Vorbedingungen und Invarianten den Vertrag zwischen Aufrufer und Implementierer. Vorbedingungen beschränken, welche Eingaben zulässig sind; Nachbedingungen garantieren das Ergebnis und den finalen Zustand nach erfolgreicher Ausführung.

Formale Darstellung und Beispiele. In formalen Spezifikationen lassen sich Nachbedingungen als Q nach dem Ausführen C formulieren: {P} C {Q}. Beispiel: Funktion max(a,b) gibt den größeren Wert zurück. Vorbedingung: keine oder die Eingaben müssen definiert sein. Nachbedingung: result >= a und result >= b, und (result == a oder result == b). Beispiel2: Funktion sumTo(n) berechnet 1+...+n. Vorbedingung: n >= 0. Nachbedingung: result == n*(n+1)/2.

Verifikation und Praxis: Nachbedingungen können durch Laufzeitprüfungen (Runtime-Assertion Checks) überwacht werden, durch formale Verifikation oder durch Tests abgedeckt. Sie dienen der Dokumentation und der Fehlersuche. Wichtig ist, Nachbedingungen aktuell zu halten, wenn sich Implementierung oder Anforderungen ändern. Einschränkungen: zu starke oder widersprüchliche Nachbedingungen erschweren die Wartung und können falsche Annahmen verbergen.