Nachbedingung - Postcondition

In der Computerprogrammierung ist eine Nachbedingung eine Bedingung oder ein Prädikat , das direkt nach der Ausführung eines Codeabschnitts oder nach einer Operation in einer formalen Spezifikation immer wahr sein muss . Nachbedingungen werden manchmal mithilfe von Assertions innerhalb des Codes selbst getestet . Häufig werden Nachbedingungen einfach in die Dokumentation des betroffenen Codeabschnitts aufgenommen.

Zum Beispiel: Das Ergebnis einer Fakultät ist immer eine ganze Zahl und größer oder gleich 1. Ein Programm, das die Fakultät einer eingegebenen Zahl berechnet, hat also Nachbedingungen, dass das Ergebnis nach der Berechnung eine ganze Zahl ist und dass es größer als oder . ist gleich 1. Ein weiteres Beispiel: Ein Programm, das die Quadratwurzel einer eingegebenen Zahl berechnet, könnte die Nachbedingung haben, dass das Ergebnis eine Zahl ist und dass ihr Quadrat gleich der Eingabe ist.

Nachbedingungen in der objektorientierten Programmierung

In einigen Software - Design, Nachbedingungen sowie Ansätze Voraussetzungen und Klasse Invarianten , sind Komponenten der Software Bauverfahren Design by Contract .

Die Nachbedingung für jede Routine ist eine Deklaration der Eigenschaften, die nach Abschluss der Ausführung der Routine garantiert werden. In Bezug auf den Vertrag der Routine bietet die Nachbedingung potentiellen Aufrufern die Gewissheit, dass in Fällen, in denen die Routine in einem Zustand aufgerufen wird, in dem ihre Vorbedingung gilt, die durch die Nachbedingung deklarierten Eigenschaften gewährleistet sind.

Eiffel-Beispiel

Das folgende in Eiffel geschriebene Beispiel legt den Wert eines Klassenattributs hourbasierend auf einem vom Aufrufer bereitgestellten Argument fest a_hour. Die Nachbedingung folgt dem Schlüsselwort ensure. In diesem Beispiel garantiert die Nachbedingung in Fällen, in denen die Vorbedingung gilt (dh wenn a_houreine gültige Stunde des Tages repräsentiert), dass nach der Ausführung von set_hourdas Klassenattribut hourdenselben Wert wie hat a_hour. Das Tag " hour_set:" beschreibt diese Postcondition-Klausel und dient dazu, sie im Falle einer Laufzeit-Postcondition-Verletzung zu identifizieren. 

    set_hour (a_hour: INTEGER)
            -- Set `hour' to `a_hour'
        require
            valid_argument: 0 <= a_hour and a_hour <= 23
        do
            hour := a_hour
        ensure
            hour_set: hour = a_hour
        end

Nachbedingungen und Vererbung

Wenn inheritance vorhanden ist , tun dies die Routinen, die von Nachkommenklassen (Unterklassen) geerbt werden, mit ihren Verträgen, d. h. ihren Vor- und Nachbedingungen. Dies bedeutet, dass alle Implementierungen oder Neudefinitionen von geerbten Routinen ebenfalls geschrieben werden müssen, um ihren vererbten Verträgen zu entsprechen. Nachbedingungen können in neu definierten Routinen modifiziert, aber nur verstärkt werden. Das heißt, die neu definierte Routine kann die Vorteile, die sie dem Kunden bietet, erhöhen, diese Vorteile jedoch nicht verringern.

Siehe auch

Verweise