= Solution
Use two finite <integer> <lists> $A,B$, 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 $A'=x:A$ and $B'=B$; `pushb(x)` symmetrically gives $B'=x:B$ and $A'=A$. The <precondition> of `popa` is $A\ne[]$, and its <postcondition> is return value $\operatorname{head}(A)$, new state $A'=\operatorname{tail}(A)$, and unchanged $B$. The specification for `popb` exchanges $A,B$. 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.
Back to article page
