Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:assert_and_error_conditions [2009/03/12 16:12] vkuncak |
sav08:assert_and_error_conditions [2010/03/08 13:48] vkuncak |
||
|---|---|---|---|
| Line 18: | Line 18: | ||
| wp(assert(false); assume(false),Q) = false | wp(assert(false); assume(false),Q) = false | ||
| wp(assume(false); assert(false),Q) = true | wp(assume(false); assert(false),Q) = true | ||
| - | so cannot have $\mbox{assume(false)} = \emptyset$ any more. | + | so cannot have $\mbox{assume(false)} = \emptyset$ any more, otherwise both |
| + | assert(false); assume(false) | ||
| + | assume(false); assert(false) | ||
| + | would denote empty relations. | ||
| ===== Error Variable and Good States ===== | ===== Error Variable and Good States ===== | ||
| Line 45: | 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 51: | 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') \} \\ | ||