Die algebraische Modellierung ist etwas mühsam und benötigt die Hilfsfunktionen first und rest vor allem wegen einiger Unvollkommenheiten der üblichen mathematischen Notation.
ADT Queues(T) ISWir besprechen einige Realisierungen im Einzelnen; man macht dabei leicht Fehler, weil es nicht nur den Sonderfall der leeren Schlange zu berücksichtigen gilt, sondern auch den Fall einer einelementigen Schlange, bei der Kopf und Schwanz identisch sind.
SORTS:
queue, T, boolean, cardinal
OPERATIONS:
newqueue: queue
enqueue: T queue queue
isempty: queue boolean
length: queue cardinal
dequeue: queue T queue
first: queue T
rest: queue queue
RULES:
isempty(newqueue) = true
isempty(enqueue(x, q)) = false
length(newqueue) = 0
length(enqueue(x, q)) = length(q) + 1
dequeue(q) = <first(q), rest(q)>
first(enqueue(x, q)) = IF isempty(q) THEN x ELSE first(q)
rest(enqueue(x, q)) = IF isempty(q) THEN newqueue
ELSE enqueue(x, rest(q))
END Queues.