Commit 7e2d2dbc authored by Ralf Jung's avatar Ralf Jung

WP def.n tweaking

parent c2f75971
Pipeline #5887 passed with stages
in 7 minutes and 8 seconds
...@@ -246,8 +246,8 @@ ...@@ -246,8 +246,8 @@
\newcommand{\fixp}{\mathit{fix}} \newcommand{\fixp}{\mathit{fix}}
%% various pieces of Syntax %% various pieces of Syntax
\def\MU #1.{\mu #1.\spac}% \def\MU #1.{\mu\,#1.\spac}%
\def\Lam #1.{\lambda #1.\spac}% \def\Lam #1.{\lambda\,#1.\spac}%
\newcommand{\proves}{\vdash} \newcommand{\proves}{\vdash}
\newcommand{\provesIff}{\mathrel{\dashv\vdash}} \newcommand{\provesIff}{\mathrel{\dashv\vdash}}
...@@ -259,8 +259,8 @@ ...@@ -259,8 +259,8 @@
\newcommand{\gmapsto}{\hookrightarrow}% \newcommand{\gmapsto}{\hookrightarrow}%
\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}% \newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%
\NewDocumentCommand\wpre{m O{} m}% \NewDocumentCommand\wpre{o m O{} m}%
{\textlog{wp}_{#2}\spac#1\spac{\left\{#3\right\}}} {\textlog{wp}{\IfValueT{#1}{(#1)}}_{#3}\spac#2\spac{\left\{#4\right\}}}
\newcommand{\stateinterp}{S} \newcommand{\stateinterp}{S}
......
...@@ -161,13 +161,13 @@ This can be instantiated, for example, with ownership of an authoritative RA to ...@@ -161,13 +161,13 @@ This can be instantiated, for example, with ownership of an authoritative RA to
Finally, weakest precondition takes a parameter $\stuckness \in \set{\NotStuck, \MaybeStuck}$ indicating whether program execution is allowed to get stuck. Finally, weakest precondition takes a parameter $\stuckness \in \set{\NotStuck, \MaybeStuck}$ indicating whether program execution is allowed to get stuck.
\begin{align*} \begin{align*}
\textdom{wp}_\stuckness \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\ \textdom{wp}(\stateinterp, \stuckness) \eqdef{}& \MU \textdom{wp\any rec}. \Lam \mask, \expr, \pred. \\
& (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\ & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
& \Bigl(\toval(\expr) = \bot \land \All \state. \stateinterp(\state) \vsW[\mask][\emptyset] {}\\ & \Bigl(\toval(\expr) = \bot \land \All \state. \stateinterp(\state) \vsW[\mask][\emptyset] {}\\
&\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\ &\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\
&\qquad\qquad \stateinterp(\state') * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\ &\qquad\qquad \stateinterp(\state') * \textdom{wp\any rec}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp\any rec}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\
% (* value case *) % (* value case *)
\wpre\expr[\stuckness;\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}_\stuckness(\mask, \expr, \Lam\val.\prop) \wpre[\stateinterp]\expr[\stuckness;\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\stateinterp,\stuckness)(\mask, \expr, \Lam\val.\prop)
\end{align*} \end{align*}
If we leave away the mask $\mask$, we assume it to default to $\top$. If we leave away the mask $\mask$, we assume it to default to $\top$.
If we leave away the stuckness $\stuckness$, it defaults to $\NotStuck$. If we leave away the stuckness $\stuckness$, it defaults to $\NotStuck$.
......
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