Theory List_Spec
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.›