Solution (source code)

= Solution

Store characters in a mutable <dynamic array>. Its length is maintained by the collection, giving constant-time `size`.
``
class DocImpl extends Doc {
  private val text = scala.collection.mutable.ArrayBuffer.empty[Char]
  def insert(x: Char, pos: Int): Unit = {
    require(0 <= pos && pos <= text.length)
    text.insert(pos, x)
  }
  def delete(pos: Int): Char = {
    require(0 <= pos && pos < text.length)
    text.remove(pos)
  }
  def read(pos: Int): Char = {
    require(0 <= pos && pos < text.length)
    text(pos)
  }
  def size: Int = text.length
}
``
The <representation invariant> requires a nonnull private <dynamic array> containing a finite <sequence> of characters, with its internal collection invariant maintained by the library. The <abstraction function> is
$$
\boxed{\alpha(\mathrm{text})=\langle\mathrm{text}(0),\ldots,\mathrm{text}(\mathrm{length}-1)\rangle.}
$$
Insertion allows the end position and shifts the suffix right; deletion returns exactly the removed character and shifts the suffix left. `read` leaves the abstract state unchanged. `size` equals the abstract <sequence> length in $O(1)$ <time complexity>. Indexed reads are also constant time; insertion and deletion may take linear time, which the question permits.