Design by Contract

Definition

Beispiele

Beispiel 1

public class Kreis
{
    private double radius;

    public Kreis(double radius)
    {
        if (radius <= 0)
            throw new IllegalArgumentException("Radius muss positiv sein");

        this.radius = radius;
    }

    public void vergroessern(double faktor)
    {
        if (faktor <= 0)
            throw new IllegalArgumentException("Faktor muss positiv sein");

        radius *= faktor;
    }

    public double berechneFlaeche()
    {
        return Math.PI * radius * radius;
    }
}

Vorbedingungen:

Der Parameter radius im Konstruktor muss positiv sein

Der Parameter faktor in der Methode vergroessern() muss positiv sein

Nachbedingungen:

Die Methode vergroessern() hat den Radius um exakt den angegebenen Faktor vergrößert.

Invarianten:

Die Bedingung radius > 0 gilt jederzeit, egal welche Methode gerade ausgeführt wurde.

Beispiel 2

Stellen wir uns eine Warteschlange vor, die nach dem FIFO-Prinzip arbeitet (first in, first out). Eine Klasse Queue stelt nun folgende Methoden zur Verfügung:

1. public Queue (int capacity) // Konstruktor
2. public void enqueue(String value)
3. public void dequeue()
4. public String front()
5. public int size()

Vorbedingungen:

• Konstruktor: Der Parameter capacity muss > 0 sein
• enqueue(): Die Kapazität darf noch nicht erreicht sein
• dequeue(): Die Warteschlange darf nicht leer sein
• front(): Die Warteschlange darf nicht leer sein

Nachbedingungen:

• Konstruktor: Es wurde eine Queue mit capacity Plätzen erzeugt
• enqueue(): Die Anzahl der Elemente wurde um 1 erhöht und das neue Element befindet sich am Ende der Schlange
• dequeue(): Die Anzahl der Elemente wurde um 1 erniedrigt, das zuerst eingefügte (vordere) Element wurde entfernt.
• front(): Die Anzahl der Elemente wurde nicht verändert, das zuerst eingefügte (vordere) Element wird als Wert zurückgegeben.
• size(): Die Zahl der vorhandenen Elemente wird zurückgegeben und die Zahl der Elemente wurde nicht verändert.

Invarianten:

Egal, welche Methode gerade ausgeführt wurde, gilt:

• 0 <= n <= capacity // n = Anzahl der vorhandenen Elemente
• Alle belegten Felder liegen im Bereich 0 bis capacity - 1, wenn die Queue mithilfe eines Arrays implementiert wurde.
• Die FIFO-Reihenfolge bleibt erhalten

Dieses zweite Beispiel zeigt sehr gut, wie wichtig es ist, dass der interne Zustand eines Objektes wie einer Queue immer konsistent bleibt, unabhängig davon, wie oft enqueue(), dequeue() oder eine der anderen Methoden ausgeführt wurde. Gerade bei Datenstrukturen, die Abstrakte Datentypen verwirklichen (Stack, Queue, List etc.) sind Invarianten eine Garantie für Konsistenz.