Theory Challenge1
chapter ‹Gap Buffer›
section ‹Challenge›
text_raw ‹{\upshape
A gap buffer is a data structure for the implementation of text editors,
which can efficiently move the cursor, as well add and delete characters.
The idea is simple: the editor's content is represented as a character array~$a$
of length~$n$,
which has a gap of unused entries $a[l], \ldots, a[r-1]$,
with respect to two indices $l \le r$.
The data it represents is composed as $a[0], \ldots, a[l-1], a[r], ..., a[n-1]$.
The current cursor position is at the left index $l$, and if we type a character, it is
written to $a[l]$ and $l$ is increased.
When the gap becomes empty, the array is enlarged and the data from $r$ is shifted to the right.
\paragraph{Implementation task.}
Implement the following four operations in the language of your tool:
Procedures \verb|left()| and \verb|right()| move the cursor by one character;
\verb|insert()| places a character at the beginning of the gap $a[l]$;
\verb|delete()| removes the character at $a[l]$ from the range of text.
\begin{multicols}{2}
\begin{lstlisting}[language=C,morekeywords={procedure,function,end,to,in,var,then,not,mod}]
procedure left()
if l != 0 then
l := l - 1
r := r - 1
a[r] := a[l]
end-if
end-procedure
procedure right()
// your task: similar to left()
// but pay attention to the
// order of statements
end-procedure
\end{lstlisting}
\begin{lstlisting}[language=C,morekeywords={procedure,function,end,to,in,var,then,not,mod}]
procedure insert(x: char)
if l == r then
// see extended task
grow()
end-if
a[l] := x
l := l + 1
end-procedure
procedure delete()
if l != 0 then
l := l - 1
end-if
end-procedure
\end{lstlisting}
\end{multicols}
\paragraph{Verification task.}
Specify the intended behavior of the buffer in terms of a contiguous
representation of the editor content.
This can for example be based on strings, functional arrays, sequences, or lists.
Verify that the gap buffer implementation satisfies this specification,
and that every access to the array is within bounds.
\emph{Hint:}
For this task you may assume that \verb|insert()| has the
precondition $l < r$ and remove the call to \verb|grow()|.
Alternatively, assume a contract for \verb|grow()| that ensures
that this call does not change the abstract representation.
\paragraph{Extended verification task.}
Implement the operation \verb|grow()|, specify its behavior in a way that lets
you verify \verb|insert()| in a modular way
(i.e. not by referring to the implementation of \verb|grow()|),
and verify that \verb|grow()| satisfies this specification.
\emph{Hint}: You may assume that the allocation of the new buffer always succeeds.
If~your tool/language supports copying array ranges (such as
\verb|System.arraycopy()| in Java),
consider using these primitives instead of the loops in the
pseudo-code below.
\begin{lstlisting}[language=C,morekeywords={procedure,function,end,to,in,new,var,then,not,mod}]
procedure grow()
var b := new char[a.length + K]
// b[0..l] := a[0..l]
for i = 0 to l - 1 do
b[i] := a[i]
end-for
// b[r + K..] := a[r..]
for i = r to a.length - 1 do
b[i + K] := a[i]
end-for
r := r + K
a := b
end-procedure
\end{lstlisting}
\paragraph{Resources}
\begin{itemize}
\item \url{https://en.wikipedia.org/wiki/Gap_buffer}
\item \url{http://scienceblogs.com/goodmath/2009/02/18/gap-buffers-or-why-bother-with-1}
\end{itemize}
}
\clearpage
›
section ‹Solution›
theory Challenge1
imports "lib/VTcomp"
begin
text ‹Fully fledged specification of textbuffer ADT,
and its implementation by a gap buffer.
›
subsection ‹Abstract Specification›
text ‹
Initially, we modelled the abstract text as a cursor position and a list.
However, this gives you an invariant on the abstract level. An isomorphic
but invariant free formulation is a pair of lists, representing the text
before and after the cursor.
›