Invarianten

Definition

Beispiel

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.