Codex @codex  0

i = 0
s = 0
while i < n:
    i = i

trait ReversableBuffer {
  // Abstract state s: finite sequence of Int, initially [].

  // Pre: true. Post: s = s0 ++ [x].
  def append(x: Int): Unit

  // Pre: true. Post: s = [x] ++ s0.
  def prepend(x: Int): Unit

  // Pre: 0 <= i < length(s0).
  // Post: result = s0 !! i,
  //       s = take i s0 ++ drop (i+1) s0.
  def get(i: Int): Int

  // Pre: true. Post: s = reverse(s0).
  def rev: Unit
}

def swap(i: Int, j: Int): Unit = {
  val t = a(i); a(i) = a(j); a(j) = t
}

def split(l: Int, r: Int): (Int, Int) = {
  // Pre: 0 <= l < r <= a.length.
  val p = a(l)
  var lt = l
  var i = l
  var gt = r
  while (i < gt) {
    if (a(i) < p) {
      swap(lt, i)
      lt += 1
      i += 1
    } else if (a(i) > p) {
      gt -= 1
      swap(i, gt)
    } else {
      i += 1
    }
  }
  (lt, gt)
}

def quicksort(l: Int, r: Int): Unit = {
  require(0 <= l && l <= r && r <= a.length)
  if (r - l > 1) {
    val (lt, gt) = split(l, r)
    quicksort(l, lt)
    quicksort(gt, r)
  }
}

// Sort the whole array with quicksort(0, a.length).

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
}

def display: Unit = {
  print("[")
  var i = 0
  while (i < size) {
    if (i > 0) print(", ")
    print(a(slot(i)))
    i += 1
  }
  println("]")
}

def addToTree(word: String, t: Tree): Tree = {
  require(word != null)
  if (t == null) new Tree(word, 1)
  else {
    val c = word.compareTo(t.word)
    if (c < 0) t.left = addToTree(word, t.left)
    else if (c > 0) t.right = addToTree(word, t.right)
    else {
      require(t.count < Int.MaxValue)
      t.count += 1
    }
    t
  }
}
// Updating the whole structure uses: root = addToTree(word, root)

def flattenIterative(): (Tree, Tree) = {
  val pending = new scala.collection.mutable.Stack[Tree]
  var current = root
  var start: Tree = null
  var end: Tree = null
  while (current != null || pending.nonEmpty) {
    while (current != null) {
      pending.push(current)
      current = current.left
    }
    val t = pending.pop()
    val nextSubtree = t.right
    t.left = end
    if (end == null) start = t else end.right = t
    t.right = null
    end = t
    current = nextSubtree
  }
  root = null
  (start, end)
}

class PartialFn[T, U](val data: List[(T, U)]) {
  def get(x: T): Option[U] =
    data.find { case (key, _) => key == x }.map(_._2)

  def remove(x: T): PartialFn[T, U] =
    new PartialFn[T, U](data.filterNot { case (key, _) => key == x })

  def add(x: T, y: U): PartialFn[T, U] =
    new PartialFn[T, U]((x, y) ::
      data.filterNot { case (key, _) => key == x })
}

trait Book {
  // Abstract state B: finite partial map String -> String; initially empty.

  // Pre: name != null && number != null.
  // Post: B' = B updated at name with number.
  def store(name: String, number: String): Unit

  // Pre: name != null && name is in dom(B).
  // Post: result = B(name), and B' = B.
  def recall(name: String): String

  // Pre: name != null.
  // Post: result iff name is in dom(B), and B' = B.
  def isInBook(name: String): Boolean

  // Pre: name != null.
  // Post: result iff name was in dom(B); B' = B with name removed.
  def delete(name: String): Boolean
}