Commit 7dad46a3 by Ralf Jung

### docs: fix adequacy for state invariant-style WP

parent 7b221fa8
 ... @@ -340,33 +340,31 @@ The purpose of the adequacy statement is to show that our notion of weakest prec ... @@ -340,33 +340,31 @@ The purpose of the adequacy statement is to show that our notion of weakest prec There are two properties we are looking for: First of all, the postcondition should reflect actual properties of the values the program can terminate with. There are two properties we are looking for: First of all, the postcondition should reflect actual properties of the values the program can terminate with. Second, a proof of a weakest precondition with any postcondition should imply that the program is \emph{safe}, \ie that it does not get stuck. Second, a proof of a weakest precondition with any postcondition should imply that the program is \emph{safe}, \ie that it does not get stuck. To express the adequacy statement for functional correctness, we assume we are given some set $V \subseteq \Val$ of legal return values. \begin{defn}[Adequacy] Furthermore, we assume that the signature $\Sig$ adds a predicate $\pred$ to the logic which reflects $V$ into the logic: A program $\expr$ in some initial state $\state$ is \emph{adequate} for a set $V \subseteq \Val$ of legal return values ($\expr, \state \vDash V$) if for all $\tpool', \state'$ such that $([\expr], \state) \tpstep^\ast (\tpool', \state')$ we have \begin{enumerate} \item Safety: For any $\expr' \in \tpool'$ we have that either $\expr'$ is a value, or $$\red(\expr'_i,\state')$$: $\All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state')$ Notice that this is stronger than saying that the thread pool can reduce; we actually assert that \emph{every} non-finished thread can take a step. \item Legal return value: If $\tpool'_1$ (the main thread) is a value $\val'$, then $\val' \in V$: $\All \val',\tpool''. \tpool' = [\val'] \dplus \tpool' \Ra \val' \in V$ \end{enumerate} \end{defn} To express the adequacy statement for functional correctness, we assume that the signature $\Sig$ adds a predicate $\pred$ to the logic which reflects the set $V$ of legal return values into the logic: $\begin{array}{rMcMl} \[\begin{array}{rMcMl} \Sem\pred &:& \Sem{\Val\,} \nfn \Sem\Prop \\ \Sem\pred &:& \Sem{\Val\,} \nfn \Sem\Prop \\ \Sem\pred &\eqdef& \Lam \val. \Lam \any. \setComp{n}{v \in V} \Sem\pred &\eqdef& \Lam \val. \Lam \any. \setComp{n}{v \in V} \end{array}$ \end{array}\] The signature can of course state arbitrary additional properties of $\pred$, as long as they are proven sound. 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: The adequacy statement now reads as follows: \begin{align*} \begin{align*} &\All \mask, \expr, \val, \pred, \state, \state', \tpool'. &\All \mask, \expr, \val, \pred, \state. \\&( \ownPhys\state \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra \\&( \TRUE \proves {\upd}_\mask \Exists S. S(\state) * \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra \\&\cfg{\state}{[\expr]} \step^\ast \\&\expr, \state \vDash V \cfg{\state'}{[\val] \dplus \tpool'} \Ra \\&\val \in V \end{align*} The adequacy statement for safety says that our weakest preconditions imply that every expression in the thread pool either is a value, or can reduce further. \begin{align*} &\All \mask, \expr, \state, \state', \tpool'. \\&(\All n. \melt \in \mval_n) \Ra \\&( \ownPhys\state \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra \\&\cfg{\state}{[\expr]} \step^\ast \cfg{\state'}{\tpool'} \Ra \\&\All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state') \end{align*} \end{align*} Notice that this is stronger than saying that the thread pool can reduce; we actually assert that \emph{every} non-finished thread can take a step. 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. \paragraph{Hoare triples.} \paragraph{Hoare triples.} It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs in Coq. It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs in Coq. ... ...
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