 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^{\prime }=x:A$ and $B^{\prime }=B$; pushb(x) symmetrically gives $B^{\prime }=x:B$ and $A^{\prime }=A$. The precondition of popa is $A\ne []$, and its postcondition is return value $\mathrm{head}(A)$, new state $A^{\prime }=\mathrm{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.