Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:assert_and_error_conditions [2009/03/12 16:17] vkuncak |
sav08:assert_and_error_conditions [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 28: | Line 28: | ||
We assume that the desired properties $P$ satisfy | We assume that the desired properties $P$ satisfy | ||
- | \[ | + | \begin{equation*} |
\models P \rightarrow OK | \models P \rightarrow OK | ||
- | \] | + | \end{equation*} |
===== Desired Rules for Weakest Preconditions ===== | ===== Desired Rules for Weakest Preconditions ===== | ||
For all $Q$ such that $\models Q \rightarrow OK$, we would like the following to hold: | For all $Q$ such that $\models Q \rightarrow OK$, we would like the following to hold: | ||
- | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
\models wp(c,Q) \rightarrow OK \\ | \models wp(c,Q) \rightarrow OK \\ | ||
wp(c1 [] c2,Q) = wp(c1,Q) \land wp(c2,Q) \\ | wp(c1 [] c2,Q) = wp(c1,Q) \land wp(c2,Q) \\ | ||
Line 43: | Line 43: | ||
wp(assume(F),Q) = (OK \land (F \rightarrow Q)) \\ | wp(assume(F),Q) = (OK \land (F \rightarrow Q)) \\ | ||
wp(assert(F),Q) = (F \land Q) | wp(assert(F),Q) = (F \land Q) | ||
- | \end{array}\] | + | \end{array}\end{equation*} |
We assume above that $x$ is not the //error// variable. | We assume above that $x$ is not the //error// variable. | ||
Note: we wrote $OK \land ...$ in the weakest precondition of assume, but usually $OK$ is implicit and we do not write it. We do not need it in other cases because it follows that right hand side implies $OK$. | Note: we wrote $OK \land ...$ in the weakest precondition of assume, but usually $OK$ is implicit and we do not write it. We do not need it in other cases because it follows that right hand side implies $OK$. | ||
+ | |||
Line 54: | Line 55: | ||
Let OK denote s(error)=0 and OK' denote s'(error)=0. We define: | Let OK denote s(error)=0 and OK' denote s'(error)=0. We define: | ||
\begin{eqnarray*} | \begin{eqnarray*} | ||
- | R_c(\mbox{havoc(x)}) &=& \{(s,s') \mid OK \rightarrow (OK' \land s'(y)=s(y)) \} \\ | + | R_c(\mbox{havoc(x)}) &=& \{(s,s') \mid OK \rightarrow (OK' \land \bigwedge_{y \not\equiv x}\ s'(y)=s(y)) \} \\ |
R_c(\mbox{assert}\ F}) &=& \{(s,s') \mid (OK \land F(s)) \rightarrow s=s' \} \\ | R_c(\mbox{assert}\ F}) &=& \{(s,s') \mid (OK \land F(s)) \rightarrow s=s' \} \\ | ||
R_c(\mbox{assume}\ F}) &=& \{(s,s') \mid OK\ \rightarrow\ (F(s) \land s=s') \} \\ | R_c(\mbox{assume}\ F}) &=& \{(s,s') \mid OK\ \rightarrow\ (F(s) \land s=s') \} \\ |