From 6bd506542f989ab254ee32538b2ad64069872edf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 12 Jan 2017 14:53:30 +0100
Subject: [PATCH] fix adequacy stmt
---
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 e2f5e9086..34a9dbfcc 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -360,7 +360,7 @@ To express the adequacy statement for functional correctness, we assume that the
The signature can of course state arbitrary additional properties of $\pred$, as long as they are proven sound.
The adequacy statement now reads as follows:
\begin{align*}
- &\All \mask, \expr, \val, \pred, \state.
+ &\All \mask, \expr, \val, \state.
\\&( \TRUE \proves {\upd}_\mask \Exists S. S(\state) * \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
\\&\expr, \state \vDash V
\end{align*}
--
GitLab