Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:assert_and_error_conditions [2010/03/08 13:48] vkuncak |
sav08:assert_and_error_conditions [2010/03/08 13:49] vkuncak |
||
|---|---|---|---|
| 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') \} \\ | ||