Abitur
14.10 Der ADT Stack - eine axiomatische Sicht
Betrachten wir noch einmal die „gewöhnliche„ Definition des ADT Stack:
Der ADT StackDer Abstrakte Datentyp Stack wird durch folgende Operationen definiert: Init(): Erzeugt einen leeren Stack. Push(x): Das Element x wird hinzugefügt. Pop(): Das zuletzt hinzugefügte Element wird entfernt. Ein Wert wird von Pop() nicht zurückgeliefert. Top(): Der Wert des zuletzt hinzugefügten Elementes wird zurückgeliefert. Dieses Element wird aber nicht entfernt! Empty(): Falls der Stack leer ist, wird TRUE zurückgeliefert, sonst FALSE. |
1 Definition des ADT Stack
Phrasen wie „das zuletzt hinzugefügte Element" sind natürlich nicht besonders wissenschaftlich oder mathematisch exakt, daher hat man es sich in der theoretischen Informatik angewöhnt, ADTs mithilfe von Axiomen zu definieren. Wie das geht, zeigt folgendes Beispiel aus dem Buch „Programmierung und Datenstrukturen" von Nievergelt und Hinrichs (1986):
2 Zitat aus dem Buch von NIEVERGELT/HINRICHS
Wir wollen die sechs Axiome schrittweise „übersetzen„. Fangen wir doch gleich mit dem ersten Axiom an.
empty(z0) = true |
Dabei muss man vorausschicken, dass q immer irgend ein 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 jetzt nicht besonders neu an, aber sehen wir erst mal weiter.
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(z) = z0 |
Mit diesem Axiom wird die Tatsache beschrieben, dass nach der Initialisierung eines Stacks dieser leer ist.
empty(push(z,x))= false |
Wenn man zuerst ein Element auf den Stack pusht und danach die Operation empty ausführt, so erhält man stets das Ergebnis false. Oder auf gut Deutsch: Ein Stack, in den man etwas hineingepusht hat, kann nicht leer sein.
top(push(z,x))= x |
Das ist ein sehr wichtiges Axiom. Hier wird nämlich festgelegt, wo im Stack ein Element x durch die Push-Operation gespeichert wird: Oben im Stack. Pusht man nämlich ein Element x und ruft anschließend die Top-Operation auf, so wird genau dieses zuletzt gepushte Element zurückgeliefert.
pop(push(z,x))= z |
Auch dieses Axiom ist sehr wichtig. Hier wird nämlich die Arbeitsweise der Operation Pop festgelegt. Pop löscht immer das Element, das zuletzt mit Push auf den Stack gelegt wurde. Ruft man erst Push auf und dann Pop, so ist der Zustand des Stacks der gleiche wir vor dem Aufruf von Push.
not empty(z) ==> push(pop(z),top(z)) = z |
Das ist wohl das komplizierteste Axiom. Am liebsten hätte ich es hier unterschlagen, weil ich selbst Probleme mit der Erklärung habe. Aber ich versuche es einmal. Bitte schreiben Sie mir eine EMail, wenn ich jetzt einen Fehler machen sollte.
Wenn man das oberste Element des Stacks erst entfernt und dann wieder pusht, so ändert sich am Zustand des Stack nichts. Das Ganze funktioniert natürlich nur dann, wenn der Stack nicht leer ist.
Übung 14.9 (6 Punkte)
Entwickeln Sie ein entsprechendes System von Axiomen für den ADT Queue und - jetzt die wichtigere Teilaufgabe - erläutern Sie diese Axiome ähnlich wie hier die Axiome für den ADT Stack erläutert wurden.
zurück zu Folge 14 - Abstrakte Datentypen
Diese HTML-Seite wurde erstellt von Ulrich Helmich am 15. April 2006 und völlig neu bearbeitet am 30. Mai 2009.