Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Imperative programming (resit) / 6 / a / i / Solution

The missing preconditions are $0\le pos\le |d|$ for insertion and $0\le 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.