Commit 6a5b8e3e authored by Glen Mével's avatar Glen Mével
Browse files

remove obsolete comments

parent a6956502
......@@ -11,6 +11,7 @@
\isQueue \tview \hview \elemViewList
& \eqdef
& \ownGhost\gqueue{\authfrag \tuple{\tview, \hview, \elemViewList}}
% we omit the injection of \exm (\exinj)
\\ \hline
......@@ -18,13 +19,11 @@
\gmonos
& :
%& \listm(\authm(\statusViewLat))
& \finmapm{\Z}{\authm(\statusViewLat)}
% \authm requires an unitary CMRA; here we omit the bottom element added to the lattice
\\
\monoWitness{\offset}{\pair\status\sview}
& \eqdef
%& \ownGhost\gmonos{[\underbrace{\munit,\;...,\;\munit}_\text{$\offset$~times},\; \authfrag \pair\status\sview]}
& \ownGhost\gmonos{\mapsingleton{\offset}{\authfrag \pair\status\sview}}
\\ \hline
......@@ -42,7 +41,7 @@
\tokenW\idx{\pair\elem\eview}
& \eqdef
& \ownGhost\gtokens{\authfrag \mapsingleton{\idx}{\pair\elem\eview}}
% hide the injection \exinj and left/right injections
% we omit the injections of \exm (\exinj) and of the sum (\cinl and \cinr)
\\ \hline
......@@ -68,17 +67,13 @@
% pure assertions:
\queue = \Tuple{\reftail, \refhead, \refstatuses, \refelements}
\cr 0 \le \tail \le \head \le \tail + \capacity
%\cr \length{\statusViewList} = \capacity
%\cr \length{\elemViewList} = \head - \tail
% pointsto assertions:
\cr \pointstoAT\reftail{\mkval\tail\tview}
\cr \pointstoAT\refhead{\mkval\head\hview}
\cr \arraypointstoAT\refstatuses\statusViewList
% authoritative ghost state assertions:
\cr \ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewListInv<\tail><\head>}}
%\cr \ownGhost\gmonos{\mkList\nthAuthStatusView\idx\capacity:}
\cr \ownGhost\gmonos{%
%\mkList\nthAuthStatusView\offset\capacity:
\{
\mapbinding \offset {\authfull \nthStatusView\offset}
\mid
......
......@@ -44,13 +44,7 @@
\end{array}}
{\dequeue~\queue}
{\Lam \elem.
%\ISep{%
% 1 \leq \nbelems \isep \elem = \elem_0
% \cr \isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
% \cr \seen(\tview \sqcup \eview_0)
%}
\isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
%\isep \seen (\tview \sqcup \eview_0)
\isep \seen \tview
\isep \seen \eview_0
\isep 1 \leq \nbelems
......@@ -89,19 +83,14 @@
{\trydequeue~\queue}
{\Lam \elemopt.
\matchwithnobinder{\elemopt}
{\None }{\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList}
{\None }{%
\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList
}
{\Some{\elem_0}}{%
%\ISep{%
% 1 \leq \nbelems \isep \elem = \elem_0
% \cr \isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
% \cr \seen(\tview \sqcup \eview_0)
%}
\isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
%\isep \seen (\tview \sqcup \eview_0)
\isep \seen \tview
\isep \seen \eview_0
\isep 1 \leq \nbelems
%\isep \elem = \elem_0
}
}
......@@ -112,6 +101,3 @@
\end{figure}
% JH : TODO : serait-ce pertinent de mentionner ici la timelessness et l'objectivité de isQueue et la persistence de queueInv? Cela fait partie de la spec, à mon sens.
% GLEN: la persistance oui, la timelessness c’est peut-être trop technique ?
% GLEN: je fais figurer la persistance en post-condition de make, ce n’est pas
% idéal mais c’est le mieux que je trouve pour la présentation (plutôt que
% d’avoir des mots "persistent(queueInv)" qui flottent au milieu de la page).
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