Der ADT Stack
In dem Informatik-Lehrbuch "Programmierung und Datenstrukturen: Eine Einführung anhand von Beispielen" von Jörg NIEVERGELT (1986) wird der ADT Stack auf folgende Weise definiert:
Wir wollen die sechs Axiome schrittweise "übersetzen". Fangen wir doch gleich mit dem ersten Axiom an.
empty(q0) = true;
Dabei muss man vorausschicken, dass q immer irgendein Stack ist; genauer ein Stackzustand. Ein besonderer Zustand eines Stacks ist q0, der leere Stack.
Das Axiom besagt also, dass der Aufruf von empty genau dann den Wert true liefert, wenn der Stack leer ist. Das hört sich doch schon mal ganz einleuchtend an.
Für alle Zustände q aus der Menge der möglichen Stackzustände Q und für alle Stackelemente x aus der Menge der möglichen Stackelemente X gelten die nächsten Axiome.
init(q) = q0;
Mit diesem Axiom wird die Tatsache beschrieben, dass nach der Initialisierung eines Stacks dieser leer ist, sich also im Zustand q0 befindet.
empty(push(q,x))= FALSE
Wenn man ein Element x auf den Stack q pusht und danach empty abfragt, so erhält man stets das Ergebnis false. Oder auf gut Deutsch: Ein Stack, in den man etwas hinein gepusht hat, kann nicht leer sein.
top(push(q,x))= x
Das ist ein sehr wichtiges Axiom. Hier wird nämlich festgelegt, wo bzw. wie im Stack ein Element x durch push gespeichert wird. Das mit push gespeicherte Element wird beim Aufruf von top als Ergebnis zurück geliefert. Anschaulich kann man sich das so vorstellen, dass das Element "oben" auf den Stack gelegt wird, und dass top stets das "obere" Element zurück liefert. Wenn man auf eine räumliche Vorstellung verzichten will, kann man auch sagen: Mit top wird immer das zuletzt mit push hinzugefügte Element ermittelt.
pop(push(q,x))= q
Auch dieses Axiom ist sehr wichtig. Hier wird nämlich die Arbeitsweise von pop festgelegt. Wenn man eine Element x pusht und dann pop aufruft, hat man genau den gleichen Stackzustand q wie vorher. Anschaulich kann man sich das so vorstellen, dass as Element "oben" auf den Stack gelegt wird, und dass pop stets das "obere" bzw. das zuletzt mit push hinzugefügte Element löscht.
not empty(q) ==> push(pop(q),top(q)) = q
Das ist wohl das komplizierteste Axiom, es ist gar nicht mehr so einfach zu verstehen.
Wenn man das Element x, das top liefert (falls der Stack nicht leer ist), zunächst irgendwo speichert, dann pop aufruft und dann das gespeicherte Element wieder mit push im Stack speichert, ändert sich der Stack nicht. Anschaulich heißt das, wenn ich ein Element mit pop vom Stack nehme und das Element sofort wieder mit push in den Stack einfüge, befindet es sich an der gleichen Stelle wie vor dem Entfernen. Der Stackzustand ändert sich also nicht.
Bei dem abstrakten Datentyp Queue (Schlange) wäre das zum Beispiel nicht der Fall. Entferne ich das vorderste Element mit dequeue und füge es sofort wieder mit enqueue in die Schlange ein, befindet es sich an einer ganz anderen Stelle, nämlich am Ende der Schlange.
Der ADT Queue
Hier sehen Sie die axiomatische Definition des ADT Queue aus dem Buch von NIEVERGELT.
Aufgabe für Abiturienten (schriftlich mit anschließendem Vortrag, 12 Rohpunkte)
Erläutern Sie die sieben Axiome auf die gleiche Weise, wie ich es im obenstehenden Text mit den Stack-Axiomen gemacht habe.
Wertung: Für die ersten vier Axiome je 1 Rohpunkt, für die Axiome 5 und 6 je 2 Rohpunkte und für das letzte Axiom 4 Rohpunkte.