Imperative Programming Part 2.
The abstract FIFO queue state is a finite sequence , initially empty. Because the interface returns
Int length, use the representable-size model . Its operations are:trait Queue[A] {
// State q: finite sequence of A; initially [].
// Pre: length(q) < Int.MaxValue. Post: q = q0 ++ [x].
def enqueue(x: A): Unit
// Pre: q is nonempty. Post: return head(q0); q = tail(q0).
def dequeue(): A
// Post: q = [].
def clear(): Unit
// Post: q unchanged; return q.isEmpty.
def isEmpty: Boolean
// Post: q unchanged; return length(q).
def length: Int
}The unchanged-state clauses on the two queries are part of their postconditions.
dequeue removes exactly the oldest remaining element, while clear discards all entries regardless of the old state. The size bound can be omitted in an unbounded mathematical model, but it must be reconciled with fixed-width lengths in an implementation.final class QueueNode(val value: Int, var next: QueueNode)A null successor terminates the chain. The stored value need not be mutable for a FIFO queue, because enqueue creates a node and dequeue removes one rather than changing its payload.
private var first: QueueNode = null
private var last: QueueNode = null
private var size = 0The representation invariant requires and a finite acyclic null-terminated linked list of exactly
size nodes starting at first. When size == 0, both endpoints are null. Otherwise last is precisely the final reachable node and last.next == null.The abstraction function maps the chain from first to last to its payload sequence. Initially all pointers are null and the cached size is zero, giving the empty abstract queue. A tail pointer makes append constant-time; the cached size makes the
length query constant-time without traversing the chain.Use the trait and node definition above. The reference to a “stack” in this part is a wording error: the declared class and operations implement a FIFO queue.
class ListQueue extends Queue[Int] {
private var first: QueueNode = null
private var last: QueueNode = null
private var size = 0
def enqueue(x: Int): Unit = {
require(size < Int.MaxValue, "queue size limit")
val fresh = new QueueNode(x, null)
if (last == null) first = fresh
else last.next = fresh
last = fresh
size += 1
}
def dequeue(): Int = {
require(first != null, "empty queue")
val answer = first.value
first = first.next
size -= 1
if (first == null) last = null
answer
}
def clear(): Unit = {
first = null
last = null
size = 0
}
def isEmpty: Boolean = size == 0
def length: Int = size
}Appending links the fresh node after the old tail, or establishes both endpoints when empty. Removing the head preserves the tail unless the final node was removed, in which case both endpoints become null. Clearing only discards the endpoint references; it need not visit or overwrite unreachable nodes. Thus all operations are in the usual pointer-operation/allocation cost model, with later garbage collection excluded from an individual operation's bound. The representation invariant and abstraction function show the specified sequence changes, including empty/singleton transitions.
Articles by others on the same topic
There are currently no matching articles.