(* Martin Kleppmann, University of Cambridge Victor B. F. Gomes, University of Cambridge Dominic P. Mulligan, Arm Research, Cambridge Alastair Beresford, University of Cambridge *) section‹Relationship to Strong List Specification› text‹In this section we show that our list specification is stronger than the $\mathcal{A}_\textsf{strong}$ specification of collaborative text editing by Attiya et al.~\<^cite>‹"Attiya:2016kh"›. We do this by showing that the OpSet interpretation of any set of insertion and deletion operations satisfies all of the consistency criteria that constitute the $\mathcal{A}_\textsf{strong}$ specification. Attiya et al.'s specification is as follows~\<^cite>‹"Attiya:2016kh"›: \begin{displayquote} An abstract execution $A = (H, \textsf{vis})$ belongs to the \emph{strong list specification} $\mathcal{A}_\textsf{strong}$ if and only if there is a relation $\textsf{lo} \subseteq \textsf{elems}(A) \times \textsf{elems}(A)$, called the \emph{list order}, such that: \begin{enumerate} \item Each event $e = \mathit{do}(\mathit{op}, w) \in H$ returns a sequence of elements $w=a_0 \dots a_{n-1}$, where $a_i \in \textsf{elems}(A)$, such that \begin{enumerate} \item $w$ contains exactly the elements visible to $e$ that have been inserted, but not deleted: \[ \forall a.\; a \in w \quad\Longleftrightarrow\quad (\mathit{do}(\textsf{ins}(a, \_), \_) \le_\textsf{vis} e) \;\wedge\; \neg(\mathit{do}(\textsf{del}(a), \_) \le_\textsf{vis} e). \] \item The order of the elements is consistent with the list order: \[ \forall i, j.\; (i < j) \;\Longrightarrow\; (a_i, a_j) \in \textsf{lo}. \] \item Elements are inserted at the specified position: if $\mathit{op} = \textsf{ins}(a, k)$, then $a = a_{\mathrm{min} \{k,\; n-1\}}$. \end{enumerate} \item The list order $\textsf{lo}$ is transitive, irreflexive and total, and thus determines the order of all insert operations in the execution. \end{enumerate} \end{displayquote} This specification considers only insertion and deletion operations, but no assignment. Moreover, it considers only a single list object, not a graph of composable objects like in our paper. Thus, we prove the relationship to $\mathcal{A}_\textsf{strong}$ using a simplified interpretation function that defines only insertion and deletion on a single list.› theory List_Spec imports Insert_Spec begin text‹We first define a datatype for list operations, with two constructors: \isa{Insert ref val}, and \isa{Delete ref}. For insertion, the \isa{ref} argument is the ID of the existing element after which we want to insert, or \isa{None} to insert at the head of the list. The \isa{val} argument is an arbitrary value to associate with the list element. For deletion, the \isa{ref} argument is the ID of the existing list element to delete.›