From fedc7d8a1775b085ca46d2f1d98368f8c1a85db1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Aug 2018 12:07:13 +0200
Subject: [PATCH] Fix typo in the documentation. Thanks to Joe for pointing
that out.
---
docs/program-logic.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 69e41523b..9ae6f6638 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -272,7 +272,7 @@ The signature can of course state arbitrary additional properties of $\pred$, as
The adequacy statement now reads as follows:
\begin{align*}
&\All \mask, \expr, \val, \state.
- \\&( \TRUE \proves {\upd}_\mask \Exists \stateinterp. \stateinterp(\state) * \wpre[\stateinterp]{\expr}[\stuckness;\mask]{x.\; \pred(x)}) \Ra
+ \\&( \TRUE \proves \pvs[\mask] \Exists \stateinterp. \stateinterp(\state) * \wpre[\stateinterp]{\expr}[\stuckness;\mask]{x.\; \pred(x)}) \Ra
\\&\expr, \state \vDash_\stuckness V
\end{align*}
Notice that the state invariant $S$ used by the weakest precondition is chosen \emph{after} doing a fancy update, which allows it to depend on the names of ghost variables that are picked in that initial fancy update.
--
GitLab