Nachbedingungen

Dieser Begriff (engl.: postconditions) bezieht sich auf den Kontrakt, der zwischen einer Methode und den Benutzern dieser Methode besteht.

Wenn der Benutzer der Methode die Vorbedingungen einhält (und nur dann), ist die Methode in der Pflicht, bestimmte Nachbedingungen einzuhalten.

Die Vorbedingungen und die Nachbedingungen bilden zusammen mit den Invarianten den Kontrakt (Vertrag) der Methode (siehe auch Design-by-contract-Prinzip).

Beispiele

Beispiel 1

public int[] getElement(int[] list, int i)
{
   if (list != null)
      throw new IllegalArgumentException("Array darf nicht null sein");
   if (i < 0 || i >= list.length)
      throw new IndexOutOfBoundsException("Index außerhalb des gültigen Bereichs"
   return list[i];
}

Als Nachbedingung kann man hier erwarten, dass der Array list selbst nicht verändert wird, wenn man die Methode ausführt. Außerdem kann man erwarten, dass das Element an der Position i als Rückgabewert unverändert übergeben wird, wenn der Index innerhalb der gültigen Grenzen liegt.

Beispiel 2

public double quotient(double zaehler, double nenner)
{
   if (nenner == 0)
      throw new IllegalArgumentException("Nenner darf nicht 0 sein");
   else 
      return zaehler/nenner;
}

Hier kann man erwarten, dass die Methode den Quotienten aus Zähler und Nenner mathematisch korrekt berechnet.

Beispiel 3

   // Diese Methode führt eine binäre Suche nach der gesuchten Zahl durch

      public int contains(int[] zahlen, int suchzahl)
      {
          // Der Quelltext
		}

Die Nachbedingungen sind hier ähnlich wie in Beispiel 1. Der Array zahlen soll durch die binäre Suche nicht verändert werden.