ADT Queue

[Gast]

Hallo,

ich habe eine Frage zum abstrakten Datentyp Queue und hoffe Ihr könnt mir weiterhelfen.

Was eine Queue ist und wie diese funktioniert ist mir klar. Da sich ein ADT aus Signatur und Semantik zusammensetzt auch.

Leider stehe ich beim Verständnis der unten mit "" markieren Zeilen etwas auf dem Schlauch:

Die Signatur eine Queue ist:
emptyQueue: → QUEUE
isQueueEmpty: QUEUE → BOOL
enqueue: ELEMENT × QUEUE → QUEUE (fügt ein Element unten an)
dequeue: QUEUE → QUEUE (entfernt das vorderste Element)
head: QUEUE → ELEMENT (gibt das vorderste Element zurück, ohne es zu entfernen)

Die Semantik ist:
x: ELEMENT
q: QUEUE
isQueueEmpty(emptyQueue()) = TRUE
isQueueEmpty(enqueue (x, q)) = FALSE
head(emptyQueue()) = ERROR
"" head(enqueue(x,q)) = IF isQueueEmpty(q) THEN x ELSE head(q)""
dequeue(emptyQueue()) = ERROR
""dequeue(enqueue(x,q)) = IF isQueueEmpty(q) THEN q ELSE enqueue(x, dequeue(q))""

Kann mir hier evtl. jemand weiterhelfen und mir diese beiden Zeilen erläutern?

Das wäre super.

(Beispiel ist von wiki: http://de.wikipedia.org/wiki/Abstrakter_Datentyp#Signatur )

[Trap]

Das sind beides die Rekursionsfälle für Queues mit mehr als einem Element Inhalt.

Versuch einen Induktionsbeweis zu führen, dass die Funktionen korrekt sind. Dabei siehst du auch wie sie funktionieren.