• English only

Differences

This shows you the differences between two versions of the page.

sav08:assert_and_error_conditions [2010/03/08 13:48]
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.
Line 55: 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 \bigwedge_{{y \not\equiv x} 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') \} \\