Coupling invariant 2026-10-31
View more
A relation between abstract and concrete states used to prove data refinement. Establish it initially; show that each concrete operation simulates the specified abstract operation and restores the relation; show that returned observations agree. For a rank collection, and justify constant-time indexed queries on a sorted array.
Read the full article
Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Imperative programming (resit) / 6 / a / Solution 2026-10-31
View more
Use an immutable list as private storage and cache its length. This makes the data refinement transparent without depending on library-specific dynamic array costs:
class DocImpl extends Doc {
  private var chars: List[Char] = Nil
  private var length: Int = 0

  def size: Int = length

  def insert(x: Char, pos: Int): Unit = {
    require(0 <= pos && pos <= length)
    val parts = chars.splitAt(pos)
    chars = parts._1 ::: (x :: parts._2)
    length += 1
  }

  def delete(pos: Int): Char = {
    require(0 <= pos && pos < length)
    val parts = chars.splitAt(pos)
    val old = parts._2.head
    chars = parts._1 ::: parts._2.tail
    length -= 1
    old
  }

  def read(pos: Int): Char = {
    require(0 <= pos && pos < length)
    chars(pos)
  }
}
The representation invariant is , with chars representing the abstract document sequence. splitAt(pos) isolates exactly the prefix before the selected array index-style position. Insertion retains that prefix and the old suffix, placing the new character between them. Deletion returns the old suffix head and retains its tail. Updating the cached length by one preserves the representation invariant. read and size preserve the abstract state.
(1)
The preconditions permit insertion at the end, including position zero in an empty document, but forbid reading or deleting at the end.
Read the full article