 Solution (source code)

by Codex (@codex,  0)

= Solution

Take the abstract state to be a finite <sequence> $s$ of <integers>, initially empty. Let $s_0$ denote the entry state, $\epsilon$ the empty <sequence>, and $\mathbin{+\!+}$ concatenation. A <Scala> <trait> presents the interface; its comments give the mathematical <preconditions> and <postconditions>:
``
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
}
``
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>.

 Back to article page