Use two finite integer lists , with the head of each list representing its stack top. Initially both are empty. A suitable abstract object interface is
trait DoubleStack {
def pusha(x: Int): Unit
def pushb(x: Int): Unit
def popa: Int
def popb: Int
def isEmptya: Boolean
def isEmptyb: Boolean
}For the unbounded abstract data type, each push has no logical precondition. The postcondition of
pusha(x) is and ; pushb(x) symmetrically gives and . The precondition of popa is , and its postcondition is return value , new state , and unchanged . The specification for popb exchanges . Each emptiness query leaves both lists unchanged and returns exactly whether its corresponding list is empty.These frame conditions matter: an operation on one stack must preserve the other, not merely produce the right return value.
A fixed-capacity implementation needs a bounded contract: , and a push requires strict inequality. Pop preconditions and all successful-operation postconditions remain unchanged. An implementation that rejects full-array pushes cannot satisfy an unbounded specification promising every push; the capacity restriction must be part of the agreed abstract data type, or its resource-failure behavior must be specified.
Use one array and two boundaries
left and right. The first stack occupies indices below left and grows rightwards; the second occupies indices at least right and grows leftwards. The representation invariant isThe abstraction function isBoth lists are top-first. The unoccupied middle interval has length right - left; a push is possible exactly when this is positive. Thus every array position can be used by either stack, avoiding a rigid half-array allocation.The implementation maintains the two boundaries from part b:
class ArrayDoubleStack(val MAX: Int) extends DoubleStack {
require(MAX >= 0)
private val data = new Array[Int](MAX)
private var left = 0
private var right = MAX
def isEmptya: Boolean = left == 0
def isEmptyb: Boolean = right == MAX
def pusha(x: Int): Unit = {
require(left < right, "double stack is full")
data(left) = x
left += 1
}
def pushb(x: Int): Unit = {
require(left < right, "double stack is full")
right -= 1
data(right) = x
}
def popa: Int = {
require(left > 0, "stack a is empty")
left -= 1
data(left)
}
def popb: Int = {
require(right < MAX, "stack b is empty")
val answer = data(right)
right += 1
answer
}
}Initialization gives empty abstract lists. Each push consumes one free position next to the appropriate top; each pop returns that top and releases its position. The guards preserve the ordering of the two boundaries and prevent invalid indexing. The abstraction function shows directly that the untouched stack is unchanged. Keeping
data private prevents clients from violating the representation invariant; this strengthens encapsulation relative to a publicly exposed implementation field without changing the six required operations.All six operations run in time, with a fixed array of
MAX integers and constant extra state. Creating and zero-initializing the array takes time, outside those operation bounds. Capacity zero gives a valid always-empty bounded structure whose pushes fail their precondition. Articles by others on the same topic
There are currently no matching articles.
