= Solution
The missing <preconditions> are \b[$0\leq pos\leq|d|$ for insertion] and \b[$0\leq pos<|d|$ for deletion and indexing]. The inclusive endpoint permits appending; deletion or access at the length is invalid. Specify the initial state, for example $d=[]$, as well as the read-only <frame conditions>: indexing returns the indicated character and preserves $d$, while `length` returns $|d|$ and preserves $d$.
The insertion and deletion clauses already describe the new <sequence>, but their returned values and effects should be interpreted against the old state. For a machine-sized length, insertion also requires $|d|<Int.MaxValue$. These clauses complete the document <abstract data type> without prescribing one storage representation.
Back to article page
