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 [2010/03/08 13:49] vkuncak |
||
|---|---|---|---|
| Line 48: | Line 48: | ||
| 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') \} \\ | ||