Skip to content
GitLab
Commit 8b372030 authored by Glen Mével's avatar Glen Mével
Browse files

try to improve the Hoare triples visually

parent 85f1deec
Hide whitespace changes
Inline Side-by-side
papers/icfp2021/figure-queue-spec-sc.tex
View file @ 8b372030
%\begin{figure}
\[\begin{array}{lcr}
\[\begin{array}{@{}l@{}}
\infer{\queueInv}{\;\;\;%
\lahoareV
{\Forall \nbelems, \elemList*[]. \queueInv \isep \isQueueSC \elemList}
{\Forall \nbelems, \elemList*[]. \isQueueSC \elemList}
{\enqueue~\queue~\elem}
{\Lam \Unit. \isQueueSC {\elemListSnoc \elemList \elem}}
\;\;\;}
\\\\
\quad
\infer{\queueInv}{\;\;\;%
\lahoareV
{\Forall \nbelems, \elemList*[]. \queueInv \isep \isQueueSC \elemList}
{\Forall \nbelems, \elemList*[]. \isQueueSC \elemList}
{\dequeue~\queue}
{\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.}
......
papers/icfp2021/figure-queue-spec-seq.tex
View file @ 8b372030
%\begin{figure}
\[\begin{array}{lcr}
\[\begin{array}{@{}l@{}}
\hoareV
{\isQueueSEQ \elemList}
......
papers/icfp2021/figure-queue-spec.tex
View file @ 8b372030
\begin{figure}
\[\begin{array}{lcr}
\[\begin{array}{@{}l@{}}
\hoareV
{\seen\view_0}
......@@ -12,11 +12,12 @@
\\\\\\
\lahoareV
{\Forall \tview, \hview, \nbelems, \elemViewList*[].
\queueInv
\isep \isQueue \tview \hview \elemViewList
{\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
\\ \hphantom{\Lam\Unit.}
\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
\hphantom{, \pair\elem\view}
\isep \seen\view
}
\end{array}}
{\enqueue~\queue~\elem}
{\Lam \Unit.
\isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}
......@@ -26,32 +27,38 @@
\\\\\\
\lahoareV
{\Forall \tview, \hview, \nbelems, \elemViewList*[].
\queueInv
\isep \isQueue \tview \hview \elemViewList
{\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
\\ \hphantom{\Lam\elem.}
\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList
\isep \seen\view
}
\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)
}
%\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 \elem = \elem_0
\isep 1 \leq \nbelems
}
\\\\\\
\lahoareV
{\Forall \tview, \hview, \nbelems, \elemViewList*[].
\queueInv
\isep \isQueue \tview \hview \elemViewList
{\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
%\\ \hspace{118pt}
\\ \hspace{23pt}
\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
\hphantom{, \pair\elem\view}
\isep \seen\view
}
\end{array}}
{\tryenqueue~\queue~\elem}
{\Lam \boolval.
\matchwith{\boolval}
{\False}{\isQueue \tview \hview \elemViewList}
{\False}{\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList}
{\True }{%
\isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}
\isep \seen\hview
......@@ -61,21 +68,26 @@
\\\\\\
\lahoareV
{\Forall \tview, \hview, \nbelems, \elemViewList*[].
\queueInv
\isep \isQueue \tview \hview \elemViewList
{\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
%\\ \hspace{127pt}
\\ \hspace{26pt}
\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList
\isep \seen\view
}
\end{array}}
{\trydequeue~\queue}
{\Lam \elemopt.
\matchwith{\elemopt}
{\None }{\isQueue \tview \hview \elemViewList}
{\Some{\elem}}{%
\ISep{%
1 \leq \nbelems \isep \elem = \elem_0
\cr \isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
\cr \seen(\tview \sqcup \eview_0)
}
{\None }{\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList}
{\Some\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 \elem = \elem_0
\isep 1 \leq \nbelems
}
}
......
papers/icfp2021/notations.tex
View file @ 8b372030
......@@ -183,7 +183,7 @@
\NewDocumentCommand \MatchWith {smmmmm} {%
\IfBooleanTF#1{%
\texttt{match}\;#2\;\texttt{with} \\
\begin{array}{@{\enspace}l@{{}\rightarrow{}}l}
\begin{array}{@{\enspace}l@{{}\rightarrow{}}l@{}}
\texttt{|}\;#3 & \begin{codeblock}[] #4 \end{codeblock} \\
\texttt{|}\;#5 & \begin{codeblock}[] #6 \end{codeblock}
\end{array}
......@@ -258,7 +258,7 @@
% (using \cr inside to separate lines)
\newcommand{\ISep}[1]{%
\ISEP
\left\{\begin{array}{@{\,}l}
\left\{\begin{array}{@{\,}l@{}}
#1
\end{array}\right.
}
......@@ -272,11 +272,18 @@
\def\Exists #1.{\exists#1.\spac}%
% pattern-matching / case distinction:
%\newcommand{\matchwith}[5]{%
% \mathrm{match}\;#1\;\mathrm{with}
% \left[\begin{array}{@{\,}l@{{}\rightarrow{}}l@{}}
% #2 & #3 \\
% #4 & #5
% \end{array}\right.
%}
\newcommand{\matchwith}[5]{%
\mathrm{match}\;#1\;\mathrm{with}
\left[\begin{array}{@{\,}l@{{}\rightarrow{}}l}
#2 & #3 \\
#4 & #5
%\mathord\lor
\left[\begin{array}{@{\,}ll@{}}
#3 & \text{if }#1 = #2 \\
#5 & \text{if }#1 = #4
\end{array}\right.
}
......@@ -481,19 +488,53 @@
\anglebracket{#1}\spac{#2}\spac\anglebracket{#3}_{#4}%
}
% USAGE: \lahoareV [vertical alignment] {pre} {c} {post} [mask]
\NewDocumentCommand \lahoareV {O{c} m m m O{}}{%
{\begin{aligned}[#1]
\NewDocumentCommand \lahoareV {O{c} m m m O{}} {{%
\begin{aligned}[#1]
& \anglebracket{#2} \\
& \quad{#3} \\
& \quad {#3} \\
& {\anglebracket{#4}}_{#5}
\end{aligned}}%
}
\end{aligned}%
}}
% Hoare triples presented like inference rules,
% with two horizontal bars:
\newcommand{\HoareRule}[4]{%
\tripleinfer[#1]{#2}{#3}{#4}%
}
%\newcommand{\HoareRule}[4][]{%
% \tripleinfer[#1]{#2}{#3}{#4}%
%}
%\NewDocumentCommand \LAHoareRule {O{} m m m O{}} {%
% \tripleinfer[#1]
% {\anglebracket{#2}}
% {#3}
% {{\anglebracket{#4}}_{#5}}
%}
\makeatletter
\newlength\Hoare@widthPrePost%
\NewDocumentCommand \HoareRule {O{c} m m m O{}} {{%
% compute the max of the widths of Pre and Post:
\settowidth\Hoare@widthPrePost{\vbox{\hbox{\(#2\)}\hbox{\(#4\)}}}%
\begin{aligned}[#1]
& {\curlybracket{\makebox[\Hoare@widthPrePost][l]{\(\vphantom{\displaystyle\sum}#2\)}}} \\
\hline
& \vphantom\sum \quad {#3} \\
\hline
& {\curlybracket{\makebox[\Hoare@widthPrePost][l]{\(\vphantom{\displaystyle\sum}#4\)}}}_{#5}
\end{aligned}
}}
\NewDocumentCommand \LAHoareRule {O{c} m m m O{}} {{%
% compute the max of the widths of Pre and Post:
\settowidth\Hoare@widthPrePost{\vbox{\hbox{\(#2\)}\hbox{\(#4\)}}}%
\begin{aligned}[#1]
& {\anglebracket{\makebox[\Hoare@widthPrePost][l]{\(\vphantom{\displaystyle\sum}#2\)}}} \\
\hline
& \vphantom\sum \quad {#3} \\
\hline
& {\anglebracket{\makebox[\Hoare@widthPrePost][l]{\(\vphantom{\displaystyle\sum}#4\)}}}_{#5}
\end{aligned}
}}
\makeatother
\renewcommand\hoareV\HoareRule
\renewcommand\lahoareV\LAHoareRule
% Store access (function application):
\newcommand{\storeapp}[2]{\maplookup{#1}{#2}}
......
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