Spezifikation einer Klasse

Definition

Beispiel:

Schnittstelle der Klasse Queue

public class Queue
{
   public Queue()
   public void enqueue(Object element)
   public void dequeue()
   public Object front()
   public boolean empty()
}

Man sieht hier gut die Rückgabetypen der Methoden front() und emtpy() sowie den Parameter der Methode enqueue().

Spezifikation der Klasse Queue

Invarianten, die dauerhaft für jedes Queue-Objekt gelten:

• Die Elemente sind in der FIFO-Reihenfolge gespeichert (First in, first out)
• Die Anzahl der Elemente ist >= 0
• Die Reihenfolge der Elemente wird durch die Operationen der Queue nicht verändert.

Konstruktor

Vorbedingungen: keine

Nachbedingungen: Die Queue ist leer (empty() == true)

enqueue (Object element)

Vorbedingungen: element != null

Nachbedingungen: element wurde ans Ende der Queue angefügt, die Anzahl der Elemente wurde um 1 erhöht, die Reihenfolge der übrigen Elemente wurde nicht verändert.

dequeue()

Vorbedingungen: Die Queue ist nicht leer

Nachbedingungen: Das vorderste Element wurde entfernt, die Anzahl der Elemente wurde um 1 verringert, die Reihenfolge der Elemente wurde nicht verändert.

Object front()

Vorbedingungen: Die Queue ist nicht leer

Nachbedingungen: Das vorderste Element wird zurückgegeben, die Anzahl und die Reihenfolge der Elemente wurden nicht verändert.

boolean empty()

Vorbedingungen: keine

Nachbedingungen: Wenn die Queue leer ist, wird true zurückgegeben, andernfalls false. Die Anzahl und die Reihenfolge der Elemente wurden nicht verändert.