Take the abstract state to be a finite sequence of integers, initially empty. Let denote the entry state, the empty sequence, and concatenation. A Scala trait presents the interface; its comments give the mathematical preconditions and postconditions:The double-ended queue has no abstract capacity limit in this first specification. Both removals require nonemptiness; the query leaves the state unchanged, an instance of command-query separation.
trait DoubleEndedQueue {
// Pre: true. Post: result == s0.isEmpty and s == s0.
def isEmpty: Boolean
// Pre: true. Post: s == [x] ++ s0.
def addLeft(x: Int): Unit
// Pre: s0.nonEmpty. Post: result == s0.head, s == s0.tail.
def getLeft(): Int
// Pre: true. Post: s == s0 ++ [x].
def addRight(x: Int): Unit
// Pre: s0.nonEmpty. Post: result == s0.last, s == s0.init.
def getRight(): Int
}A fixed-size array cannot implement unbounded successful insertion. Either specify a bounded double-ended queue with an extra not-full insertion precondition, or retain the unbounded interface and specify a possible full-capacity failure. Silently overwriting an endpoint would change the stated behavior. Here use the bounded contract, with a fixed positive capacity
MAX and abstract state . Both additions require ; the other postconditions remain unchanged. The class declaration in part (c) is interpreted as implementing this explicitly revised contract, rather than as a behavioral subtype of the unrestricted contract in part (a).The concrete state is an array
a of length MAX, a first-position index head, and an occupied-entry count size. Its representation invariant isThe abstraction function is for . Unoccupied slots are unconstrained. Storing size distinguishes empty and full states even though their two circular endpoint positions coincide. MAX=1 is valid. Using a circular buffer avoids shifting entries and makes every endpoint operation constant time.The following class uses the bounded insertion contract from part (b). For
slot performs mathematical circular indexing with a wider intermediate, so even large legal indices do not overflow before reduction:class ArrayDoubleEndedQueue(val MAX: Int) extends DoubleEndedQueue {
require(MAX > 0)
private val a = new Array[Int](MAX)
private var head = 0
private var size = 0
private def slot(offset: Int): Int =
((head.toLong + offset.toLong) % MAX.toLong).toInt
private def before(i: Int): Int = if (i == 0) MAX - 1 else i - 1
private def after(i: Int): Int = if (i == MAX - 1) 0 else i + 1
def isEmpty: Boolean = size == 0
def addLeft(x: Int): Unit = {
require(size < MAX)
head = before(head)
a(head) = x
size += 1
}
def addRight(x: Int): Unit = {
require(size < MAX)
a(slot(size)) = x
size += 1
}
def getLeft(): Int = {
require(size > 0)
val x = a(head)
head = after(head)
size -= 1
x
}
def getRight(): Int = {
require(size > 0)
val x = a(slot(size - 1))
size -= 1
x
}
}addLeft, moving the first position back one slot makes the old position the new logical index one; inserting at the new position prepends x. For addRight, the old size is the first unoccupied logical index, so writing there appends x. The removals read the appropriate endpoint and exclude that slot from the occupied interval. Every operation preserves the representation invariant and realizes the abstraction function postcondition. Old contents in unused slots cannot be observed through this interface. Each operation performs a fixed number of accesses and arithmetic operations, hence has constant time and constant space per call, apart from the class's backing storage.Place this object method inside the concrete class. Its precondition is the representation invariant; its postcondition is that the abstract data type state is unchanged and its left-to-right contents have been printed in bracket notation followed by a newline:Assume ordinary sequential execution and successful output. The loop invariant is , unchanged representation, and output consisting of
def display: Unit = {
print("[")
var i = 0
while (i < size) {
if (i > 0) print(", ")
print(a(slot(i)))
i += 1
}
println("]")
}[ followed by precisely the first abstract values, separated by commas and spaces. The loop variant decreases. At exit the closing bracket completes the required display, including [] for emptiness. This takes output operations and constant space.The successive abstract sequences are , , , , , , , , and finally . The three removals return , , and , respectively. With the display convention in part (i), the output isThe capacity-four bound is never exceeded. The abstract trace is independent of which physical array slots wrap around.
20
10
10
Queue status: [30, 40, 15] Articles by others on the same topic
There are currently no matching articles.