From 558bc91595c4de7390829f3fc361b85a6fc48e1c Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Tue, 14 Nov 2017 14:40:47 -0500
Subject: [PATCH] Fix typo in definition of weakest pre.
---
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 084200b03..3541c1070 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -257,7 +257,7 @@ This can be instantiated, for example, with ownership of an authoritative RA to
\begin{align*}
\textdom{wp} \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\
- & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \prop) \lor {}\\
+ & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
& \Bigl(\toval(\expr) = \bot \land \All \state. I(\state) \vsW[\mask][\emptyset] {}\\
&\qquad \red(\expr, \state) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\
&\qquad\qquad I(\state') * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\
--
GitLab