Commit 101b65fc authored by Ralf Jung's avatar Ralf Jung
Browse files

docs: describe derived Hoare triples and view shifts

parent 6be9e689
...@@ -4,157 +4,147 @@ ...@@ -4,157 +4,147 @@
\ralf{Give the most important derived rules.} \ralf{Give the most important derived rules.}
\paragraph{Persistent assertions.}
\begin{defn}
An assertion $\prop$ is \emph{persistent} if $\prop \proves \always\prop$.
\end{defn}
Of course, $\always\prop$ is persistent for any $\prop$.
Furthermore, by the proof rules given above, $t = t'$ as well as $\ownGGhost{\munit(\melt)}$ and $\knowInv\iname\prop$ are persistent.
Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification.
In our proofs, we will implicitly add and remove $\always$ from persistent assertions as necessary, and generally treat them like normal, non-linear assumptions.
\subsection{Program logic} \subsection{Program logic}
\ralf{Sync this with Coq.} \ralf{Sync this with Coq.}
Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively: Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively:
% \[ \[
% \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \dynA{\expr}{\lambda\Ret\val.\propB}{\mask})} \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}{\lambda\Ret\val.\propB}[\mask])}
% \qquad\qquad \qquad\qquad
% \begin{aligned} \begin{aligned}
% \prop \vs[\mask_1][\mask_2] \propB &\eqdef \always{(\prop \Ra \pvsA{\propB}{\mask_1}{\mask_2})} \\ \prop \vs[\mask_1][\mask_2] \propB &\eqdef \always{(\prop \Ra \pvs[\mask_1][\mask_2] {\propB})} \\
% \prop \vsE[\mask_1][\mask_2] \propB &\eqdef \prop \vs[\mask_1][\mask_2] \propB \land \propB \vs[\mask2][\mask_1] \prop \prop \vsE[\mask_1][\mask_2] \propB &\eqdef \prop \vs[\mask_1][\mask_2] \propB \land \propB \vs[\mask2][\mask_1] \prop
% \end{aligned} \end{aligned}
% \] \]
We write just one mask for a view shift when $\mask_1 = \mask_2$. We write just one mask for a view shift when $\mask_1 = \mask_2$.
The convention for omitted masks is generous: Clearly, all of these assertions are persistent.
The convention for omitted masks is similar to the base logic:
An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts. An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts.
\paragraph{Hoare triples.} \paragraph{View shifts.}~
\begin{mathpar} The following rules can be derived for view shifts.
\inferH{Ret}
{}
{\hoare{\TRUE}{\valB}{\Ret\val. \val = \valB}[\mask]}
\and
\inferH{Bind}
{\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \\
\All \val. \hoare{\propB}{K[\val]}{\Ret\valB.\propC}[\mask]}
{\hoare{\prop}{K[\expr]}{\Ret\valB.\propC}[\mask]}
\and
\inferH{Csq}
{\prop \vs \prop' \\
\hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\
\All \val. \propB' \vs \propB}
{\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]}
\and
\inferH{Frame}
{\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]}
{\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask \uplus \mask']}
\and
\inferH{AFrame}
{\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \text{$\expr$ not a value}
}
{\hoare{\prop * \later\propC}{\expr}{\Ret\val. \propB * \propC}[\mask \uplus \mask']}
% \and
% \inferH{Fork}
% {\hoare{\prop}{\expr}{\Ret\any. \TRUE}[\top]}
% {\hoare{\later\prop * \later\propB}{\fork{\expr}}{\Ret\val. \val = \textsf{fRet} \land \propB}[\mask]}
\and
\inferH{ACsq}
{\prop \vs[\mask \uplus \mask'][\mask] \prop' \\
\hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\
\All\val. \propB' \vs[\mask][\mask \uplus \mask'] \propB \\
\physatomic{\expr}
}
{\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']}
\end{mathpar}
\paragraph{View shifts.}
\begin{mathpar} \begin{mathparpagebreakable}
\inferH{NewInv} \inferH{vs-update}
{\infinite(\mask)}
{\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}}
\and
\inferH{FpUpd}
{\melt \mupd \meltsB} {\melt \mupd \meltsB}
{\ownGGhost{\melt} \vs \exists \meltB \in \meltsB.\; \ownGGhost{\meltB}} {\ownGGhost{\melt} \vs \exists \meltB \in \meltsB.\; \ownGGhost{\meltB}}
\and \and
\inferH{VSTrans} \inferH{vs-trans}
{\prop \vs[\mask_1][\mask_2] \propB \and \propB \vs[\mask_2][\mask_3] \propC \and \mask_2 \subseteq \mask_1 \cup \mask_3} {\prop \vs[\mask_1][\mask_2] \propB \and \propB \vs[\mask_2][\mask_3] \propC \and \mask_2 \subseteq \mask_1 \cup \mask_3}
{\prop \vs[\mask_1][\mask_3] \propC} {\prop \vs[\mask_1][\mask_3] \propC}
\and \and
\inferH{VSImp} \inferH{vs-imp}
{\always{(\prop \Ra \propB)}} {\always{(\prop \Ra \propB)}}
{\prop \vs[\emptyset] \propB} {\prop \vs[\emptyset] \propB}
\and \and
\inferH{VSFrame} \inferH{vs-mask-frame}
{\prop \vs[\mask_1][\mask_2] \propB}
{\prop \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB}
\and
\inferH{vs-frame}
{\prop \vs[\mask_1][\mask_2] \propB} {\prop \vs[\mask_1][\mask_2] \propB}
{\prop * \propC \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB * \propC} {\prop * \propC \vs[\mask_1][\mask_2] \propB * \propC}
\and \and
\inferH{VSTimeless} \inferH{vs-timeless}
{\timeless{\prop}} {\timeless{\prop}}
{\later \prop \vs \prop} {\later \prop \vs \prop}
\and \and
\axiomH{InvOpen} \inferH{vs-allocI}
{\infinite(\mask)}
{\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}}
\and
\axiomH{vs-openI}
{\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop} {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop}
\and \and
\axiomH{InvClose} \axiomH{vs-closeI}
{\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE } {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE }
\end{mathpar}
\vspace{5pt}
\subsection{Derived rules} \inferHB{vs-disj}
\ralf{Move all these to the two paragraphs above.}
\paragraph{Derived structural rules.}
The following are easily derived by unfolding the sugar for Hoare triples and view shifts.
\begin{mathpar}
\inferHB{Disj}
{\hoare{\prop}{\expr}{\Ret\val.\propC}[\mask] \and \hoare{\propB}{\expr}{\Ret\val.\propC}[\mask]}
{\hoare{\prop \lor \propB}{\expr}{\Ret\val.\propC}[\mask]}
\and
\inferHB{VSDisj}
{\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC} {\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC}
{\prop \lor \propB \vs[\mask_1][\mask_2] \propC} {\prop \lor \propB \vs[\mask_1][\mask_2] \propC}
\and \and
\inferHB{Exist} \inferHB{vs-exist}
{\All \var. \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]}
{\hoare{\Exists \var. \prop}{\expr}{\Ret\val.\propB}[\mask]}
\and
\inferHB{VSExist}
{\All \var. (\prop \vs[\mask_1][\mask_2] \propB)} {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)}
{(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB} {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB}
\and \and
\inferHB{HtBox} \inferHB{vs-box}
{\always\propB \proves \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]}
{\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]}
\and
\inferHB{VsBox}
{\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC} {\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC}
{\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC} {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC}
\and \and
\inferH{False} \inferH{vs-false}
{}
{\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]}
\and
\inferH{VSFalse}
{} {}
{\FALSE \vs[\mask_1][\mask_2] \prop } {\FALSE \vs[\mask_1][\mask_2] \prop }
\end{mathpar} \end{mathparpagebreakable}
\paragraph{Derived rules for invariants.}
Invariants can be opened around atomic expressions and view shifts.
\begin{mathpar} \paragraph{Hoare triples.}
\inferH{Inv} The following rules can be derived for Hoare triples.
{\hoare{\later{\propC} * \prop }
{\expr} \begin{mathparpagebreakable}
{\Ret\val. \later{\propC} * \propB }[\mask] \inferH{Ht-ret}
\and \physatomic{\expr} {}
} {\hoare{\TRUE}{\valB}{\Ret\val. \val = \valB}[\mask]}
{\knowInv{\iname}{\propC} \proves \hoare{\prop} \and
{\expr} \inferH{Ht-bind}
{\Ret\val. \propB}[\mask \uplus \{ \iname \}] {\text{$\lctx$ is a context} \and \hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \\
\All \val. \hoare{\propB}{\lctx(\val)}{\Ret\valB.\propC}[\mask]}
{\hoare{\prop}{\lctx(\expr)}{\Ret\valB.\propC}[\mask]}
\and
\inferH{Ht-csq}
{\prop \vs \prop' \\
\hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\
\All \val. \propB' \vs \propB}
{\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]}
\and
\inferH{Ht-mask-weaken}
{\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]}
{\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask \uplus \mask']}
\\\\
\inferH{Ht-frame}
{\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]}
{\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask]}
\and
\inferH{Ht-frame-step}
{\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot}
{\hoare{\prop * \later\propC}{\expr}{\Ret\val. \propB * \propC}[\mask]}
\and
\inferH{Ht-atomic}
{\prop \vs[\mask \uplus \mask'][\mask] \prop' \\
\hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\
\All\val. \propB' \vs[\mask][\mask \uplus \mask'] \propB \\
\physatomic{\expr}
} }
{\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']}
\and
\inferHB{Ht-disj}
{\hoare{\prop}{\expr}{\Ret\val.\propC}[\mask] \and \hoare{\propB}{\expr}{\Ret\val.\propC}[\mask]}
{\hoare{\prop \lor \propB}{\expr}{\Ret\val.\propC}[\mask]}
\and
\inferHB{Ht-exist}
{\All \var. \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]}
{\hoare{\Exists \var. \prop}{\expr}{\Ret\val.\propB}[\mask]}
\and \and
\inferH{VSInv} \inferHB{Ht-box}
{\later{\prop} * \propB \vs[\mask_1][\mask_2] \later{\prop} * \propC} {\always\propB \proves \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]}
{\knowInv{\iname}{\prop} \proves \propB \vs[\mask_1 \uplus \{ \iname \}][\mask_2 \uplus \{ \iname \}] \propC} {\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]}
\end{mathpar} \and
\inferH{Ht-false}
{}
{\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]}
\end{mathparpagebreakable}
\clearpage \clearpage
\section{Derived constructions} \section{Derived constructions}
......
...@@ -135,6 +135,8 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable ...@@ -135,6 +135,8 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable
Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$. Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$. We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
\paragraph{Metavariable conventions.} \paragraph{Metavariable conventions.}
We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type: We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:
......
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