Commit dbb277ce authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Small English fixes in the sequential spec.

parent 9b68d9b9
......@@ -16,7 +16,7 @@ an item ---~if there is one~--- from the other extremity (the \emph{tail}).
A queue holding $\nbelems$ items \(\elemListWithLen\), where the left extremity
of the list is the tail and the right extremity is the head,
will be represented in separation logic with a representation predicate:
is represented in separation logic with a representation predicate:
% FP suggestion d'anglais: on n'utilise jamais le futur ("will")
% dans un article scientifique, et on écrit tout au présent.
% C'est vraiment rare qu'on ait absolument besoin du futur.
......@@ -30,16 +30,18 @@ the queue, as presented in~\fref{fig:queue:specseq}. We use the standard Hoare
triple notation, with a partial correctness meaning.
%
If we own a queue~$\queue$, then we can $\enqueue$ some item~$\elem$
to~$\queue$; if this ever returns, this will return the unit value~$\Unit$ and
give us back ownership of~$\queue$ with $\elem$ appended to its head.
into~$\queue$; if this operation ever returns, then it must return the unit value~$\Unit$ and
give us back the ownership of~$\queue$, where $\elem$ has been appended at the head.
%
Conversely, if we own a queue~$\queue$, then we can $\dequeue$ from~$\queue$; if
ever returning, this will return some item~$\elem$ which was in fact the item at
the tail of~$\queue$, and it will give us back ownership of~$\queue$ with that
first item removed. Note that $\dequeue$ cannot return when the queue is empty
($\nbelems = 0$); in this case it will loop forever, waiting for an item to be
enqueued. This is pointless in a sequential setting, but will become meaningful
in the presence of concurrency.
this operation ever returns, then it must return some item~$\elem$ which was in fact the item~$\elem_0$ found at
the tail of~$\queue$, and it gives us back the ownership of~$\queue$, where that
first item has been removed. This specification implies that $\dequeue$ cannot possibly return when the queue is empty
($\nbelems = 0$); in this case, it must loop forever.
This is pointless in a sequential setting, but becomes meaningful
in the presence of concurrency,
where it makes sense for $\dequeue$ to wait until an item is
enqueued. % (by some other thread).
\subsubsection{Specification under sequential consistency}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment