Commit 85f1deec authored by Glen Mével's avatar Glen Mével
Browse files

improve list notations

parent d39e19e9
......@@ -59,7 +59,7 @@
\left\{\begin{array}{l}
\Exists \reftail, \refhead, \refstatuses, \refelements.
\\ \Exists \tail, \tview, \head, \hview, \elemViewListWithLenInv, \statusViewListWithLen.
\\ \Exists \tail, \tview, \head, \hview, \elemViewListInv*[], \statusViewList*[].
\\ \quad \ISep{%
% pure assertions:
\queue = \Tuple{\reftail, \refhead, \refstatuses, \refelements}
......@@ -72,7 +72,7 @@
\cr \arraypointstoAT\refstatuses\statusViewList
% authoritative ghost state assertions:
\cr \ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewListInv}}
\cr \ownGhost\gmonos{\mkDotList{\ANON{\authfull \nthStatusView{##1}}}\idx\capacity}
\cr \ownGhost\gmonos{\mkList\nthAuthStatusView\idx\capacity:}
\cr \ownGhost\gtokens{%
\authfull
\left(\begin{array}{lllr@{\;}l}
......
......@@ -2,16 +2,16 @@
\[\begin{array}{lcr}
\lahoareV
{\Forall \nbelems, \elemListWithLen. \queueInv \isep \isQueueSC \elemList}
{\Forall \nbelems, \elemList*[]. \queueInv \isep \isQueueSC \elemList}
{\enqueue~\queue~\elem}
{\Lam \Unit. \isQueueSC {(\elemList + [ \elem ])}}
{\Lam \Unit. \isQueueSC {\elemListSnoc \elemList \elem}}
\\\\
\lahoareV
{\Forall \nbelems, \elemListWithLen. \queueInv \isep \isQueueSC \elemList}
{\Forall \nbelems, \elemList*[]. \queueInv \isep \isQueueSC \elemList}
{\dequeue~\queue}
{\Lam \elem. 1 \leq \nbelems \isep \elem = \elem_0 \isep \isQueueSC \elemListBWithLen}
{\Lam \elem. 1 \leq \nbelems \isep \elem = \elem_0 \isep \isQueueSC {\elemList<1>*}}
\end{array}\]
\Description{A specification of the ``queue'' data structure under sequential consistency.}
......
......@@ -4,14 +4,14 @@
\hoareV
{\isQueueSEQ \elemList}
{\enqueue~\queue~\elem}
{\Lam \Unit. \isQueueSEQ {(\elemList + [ \elem ])}}
{\Lam \Unit. \isQueueSEQ {\elemListSnoc \elemList \elem}}
\qquad
\hoareV
{\isQueueSEQ \elemList}
{\dequeue~\queue}
{\Lam \elem. 1 \leq \nbelems \isep \elem = \elem_0 \isep \isQueueSEQ \elemListBWithLen}
{\Lam \elem. 1 \leq \nbelems \isep \elem = \elem_0 \isep \isQueueSEQ {\elemList<1>*}}
\end{array}\]
\Description{A specification of the ``queue'' data structure in a sequential setting.}
......
......@@ -12,37 +12,30 @@
\\\\\\
\lahoareV
{\Forall \tview, \hview, \nbelems, \elemViewListWithLen.
{\Forall \tview, \hview, \nbelems, \elemViewList*[].
\queueInv
\isep \isQueue \tview \hview \elemViewList
\isep \seen\view
}
{\enqueue~\queue~\elem}
{\Lam \Unit.
\isQueue \tview {(\hview \sqcup \view)} {(\elemViewList + [ \pair\elem\view ])}
\isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}
\isep \seen\hview
}
\\\\\\
\lahoareV
{\Forall \tview, \hview, \nbelems, \elemViewListWithLen.
{\Forall \tview, \hview, \nbelems, \elemViewList*[].
\queueInv
\isep \isQueue \tview \hview \elemViewList
\isep \seen\view
}
{\dequeue~\queue}
%{\Lam \elem. \Exists \eview, \elemViewListB.
% \ISep{%
% \elemViewList = [ \pair\elem\eview ] + \elemViewListB
% \cr \isQueue {(\tview \sqcup \view)} \hview \elemViewListB
% \cr \seen(\tview \sqcup \eview)
% }
%}
{\Lam \elem.
\ISep{%
1 \leq \nbelems \isep \elem = \elem_0
\cr \isQueue {(\tview \sqcup \view)} \hview \elemViewListBWithLen
\cr \isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
\cr \seen(\tview \sqcup \eview_0)
}
}
......@@ -50,7 +43,7 @@
\\\\\\
\lahoareV
{\Forall \tview, \hview, \nbelems, \elemViewListWithLen.
{\Forall \tview, \hview, \nbelems, \elemViewList*[].
\queueInv
\isep \isQueue \tview \hview \elemViewList
\isep \seen\view
......@@ -60,7 +53,7 @@
\matchwith{\boolval}
{\False}{\isQueue \tview \hview \elemViewList}
{\True }{%
\isQueue \tview {(\hview \sqcup \view)} {(\elemViewList + [ \pair\elem\view ])}
\isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}
\isep \seen\hview
}
}
......@@ -68,7 +61,7 @@
\\\\\\
\lahoareV
{\Forall \tview, \hview, \nbelems, \elemViewListWithLen.
{\Forall \tview, \hview, \nbelems, \elemViewList*[].
\queueInv
\isep \isQueue \tview \hview \elemViewList
\isep \seen\view
......@@ -78,15 +71,9 @@
\matchwith{\elemopt}
{\None }{\isQueue \tview \hview \elemViewList}
{\Some{\elem}}{%
%\Exists \eview, \elemViewListB.
%\ISep{%
% \elemViewList = [ \pair\elem\eview ] + \elemViewListB
% \cr \isQueue {(\tview \sqcup \view)} \hview \elemViewListB
% \cr \seen(\tview \sqcup \eview)
%}
\ISep{%
1 \leq \nbelems \isep \elem = \elem_0
\cr \isQueue {(\tview \sqcup \view)} \hview \elemViewListBWithLen
\cr \isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
\cr \seen(\tview \sqcup \eview_0)
}
}
......
......@@ -411,17 +411,56 @@
\newcommand{\maplookup}[2]{#1(#2)}
\newcommand{\mapupdate}[3]{{#1}[\mapbinding{#2}{#3}]}
% list things (\mkList and similar are higher-order):
\newcommand{\listliteral}[1]{\left[{#1}\right]}
\newcommand{\mkListFull}[3]{\ensuremath{\listliteral{#1{#2}}_{#3}}}
\newcommand{\mkListWithLen}[3]{\mkListFull{#1}{#2}{0 \leq #2 < #3}}
\newcommand{\mkListWithLenFromOne}[3]{\mkListFull{#1}{#2}{1 \leq #2 \leq #3}}
\newcommand{\mkListWithLenFromOneExcl}[3]{\mkListFull{#1}{#2}{1 \leq #2 < #3}}
\newcommand{\mkList}[2]{\mkListFull{#1}{#2}{#2}}
\newcommand{\mkDotList}[3]{\ensuremath{\listliteral{#1{0}, ..., #1{#3-1}}}}
\newcommand{\mkDotListFromOne}[3]{\ensuremath{\listliteral{#1{1}, ..., #1{#3}}}}
\newcommand{\mkDotListFromOneExcl}[3]{\ensuremath{\listliteral{#1{1}, ..., #1{#3-1}}}}
% list things:
\newcommand{\length}[1]{\left|#1\right|}
\newcommand{\listliteral}[1]{\left[{#1}\right]}
% USAGE: \mkList {mkElem} {i} {len} [:] <start> <stop> [+] [*] [mkEncl]
% mkElem is called with an index
% i is the name to use for the index
% len is the length of the list
% : tells to display the list in extenso, with an ellipsis
% start is the first index (default 0)
% stop is one more than the last index (default `len`)
% + tells to include `stop` in the range
% * tells to make the range of the list explicit (meaningful only when
% not displayed in extenso)
% mkEncl is called with the list literal and should add some kind of
% parentheses around it (by default, square brackets are added)
\makeatletter
\NewDocumentCommand \mkList {mmm t: D<>{0} d<> t+ s O{\listliteral}} {{%
\def\mkList@elem{#1}%
\def\mkList@i{#2}%
\def\mkList@len{#3}%
\def\mkList@showDots{#4}%
\def\mkList@start{#5}%
\def\mkList@stop{#6}%
\def\mkList@stopIncluded{#7}%
\def\mkList@showRange{#8}%
\def\mkList@encl{#9}%
\expandafter\IfNoValueTF\expandafter{\mkList@stop}{
\def\mkList@stop{\mkList@len}%
}{}%
\ensuremath{%
\expandafter\IfBooleanTF\mkList@showDots{%
\expandafter\IfBooleanTF\mkList@stopIncluded{%
\mkList@encl{\mkList@elem{\mkList@start}, ..., \mkList@elem{\mkList@stop}}
}{%
\mkList@encl{\mkList@elem{\mkList@start}, ..., \mkList@elem{\mkList@stop-1}}
}
}{%
\expandafter\IfBooleanTF\mkList@showRange{%
\expandafter\IfBooleanTF\mkList@stopIncluded{%
\mkList@encl{\mkList@elem{\mkList@i}} _ {\mkList@start \leq \mkList@i \leq \mkList@stop}
}{%
\mkList@encl{\mkList@elem{\mkList@i}} _ {\mkList@start \leq \mkList@i < \mkList@stop}
}
}{%
\mkList@encl{\mkList@elem{\mkList@i}} _ {\mkList@i}
}
}
}
}}
\makeatother
% any mathematical tuple:
\newcommand{\tuple}[1]{\left(#1\right)}
......@@ -647,32 +686,21 @@
%\newcommand{\elemViewList}{\ensuremath{\mathbf{v{\hskip -0.15em}V}}}
%\newcommand{\statusViewList}{\ensuremath{\mathbf{s{\hskip -0.15em}V}}}
\newcommand{\nthElem}[1]{\elem_{#1}}
%\newcommand{\elemListWithLen}{\mkListWithLen\nthElem\idx\nbelems}
%\newcommand{\elemList}{\mkList{\ANON{\elem_{##1}}}\idx}
\newcommand{\elemListWithLen}{\mkDotList\nthElem\idx\nbelems}
\newcommand{\elemList}{\elemListWithLen}
%\newcommand{\elemListSnoc}[2]{\left(#1{} + [ #2 ]\right)}
% since we are writing lists in extenso, we can use a neater notation:
\newcommand{\elemListSnoc}[2]{\listliteral{#1[], #2}}
%\newcommand{\elemListBWithLen}{\mkListWithLenFromOneExcl\nthElem\idx\nbelems}
\newcommand{\elemListBWithLen}{\mkDotListFromOneExcl\nthElem\idx\nbelems}
\newcommand{\nthElem}[1]{\elem_{#1}}
\newcommand{\elemList}{\mkList\nthElem\idx\nbelems:}
\newcommand{\nthElemView}[1]{\pair{\elem_{#1}}{\eview_{#1}}}
%\newcommand{\elemViewListWithLen}{\mkListWithLen\nthElemView\idx\nbelems}
%\newcommand{\elemViewListWithLenInv}{\mkListWithLen\nthElemView\idx{\head-\tail}}
%\newcommand{\elemViewList}{\mkList\nthElemView\idx}
\newcommand{\elemViewListWithLen}{\mkDotList\nthElemView\idx\nbelems}
\newcommand{\elemViewListWithLenInv}{\mkDotList\nthElemView\idx{\head-\tail}}
\newcommand{\elemViewList}{\elemViewListWithLen}
\newcommand{\elemViewListInv}{\elemViewListWithLenInv}
%\newcommand{\elemViewListBWithLen}{\mkListWithLenFromOneExcl\nthElemView\idx\nbelems}
\newcommand{\elemViewListBWithLen}{\mkDotListFromOneExcl\nthElemView\idx\nbelems}
\newcommand{\elemViewList} {\mkList\nthElemView\idx\nbelems:}
\newcommand{\elemViewListInv}{\mkList\nthElemView\idx{\head-\tail}:}
\newcommand{\nthStatusView}[1]{\pair{\status_{#1}}{\sview_{#1}}}
%\newcommand{\statusViewListWithLen}{\mkListWithLen\nthStatusView\idx\capacity}
%\newcommand{\statusViewList}{\mkList\nthStatusView\idx}
\newcommand{\statusViewListWithLen}{\mkDotList\nthStatusView\idx\capacity}
\newcommand{\statusViewList}{\statusViewListWithLen}
\newcommand{\statusViewList}{\mkList\nthStatusView\idx\capacity:}
\newcommand{\nthAuthStatusView}[1]{\authfull \nthStatusView{#1}}
% an index modulo the capacity:
%\newcommand{\modcap}[1]{{#1}\mmod\capacity}
......
......@@ -12,7 +12,7 @@ an ordered list of items. It supports two main operations: \enqueue inserts
a provided item at one extremity of the queue (the \emph{head}); \dequeue extracts
an item ---~if there is one~--- from the other extremity (the \emph{tail}).
A queue holding $\nbelems$ items \(\elemListWithLen\), where the left extremity
A queue holding $\nbelems$ items \(\elemList*\), where the left extremity
of the list is the tail and the right extremity is the head,
is represented in separation logic with a representation predicate:
% FP suggestion d'anglais: on n'utilise jamais le futur ("will")
......@@ -146,7 +146,7 @@ name~$\gqueue$, that the invariant of the queue ($\queueInv$) is an additional
precondition of both operations (repeating it in the postcondition is unneeded,
as it is persistent) and that \emph{atomic} Hoare triples are used.
%
The universal quantifier ($\forall \nbelems, \elemList {.}$) is part of the
The universal quantifier ($\forall \nbelems, \elemList*[] {.}$) is part of the
syntax of an atomic triple: it binds the following variables in the precondition as
well as in the postcondition.
......
Markdown is supported
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