= Solution
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 $\mathrm{length}=\operatorname{length}(\mathrm{chars})\geq0$, 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.
$$
\boxed{\operatorname{size}:\Theta(1);\qquad\operatorname{insert},\operatorname{delete},\operatorname{read}:O(n+1).}
$$
The <preconditions> permit insertion at the end, including position zero in an empty document, but forbid reading or deleting at the end.
Back to article page
