Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:assert_and_error_conditions [2009/03/11 10:56] vkuncak |
sav08:assert_and_error_conditions [2009/03/12 16:12] vkuncak |
||
|---|---|---|---|
| Line 45: | Line 45: | ||
| 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$. | ||
| + | |||
| ===== Relational Semantics that Fulfills These Rules ===== | ===== Relational Semantics that Fulfills These Rules ===== | ||
| Line 50: | Line 51: | ||
| 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' \} \\ | + | R_c(\mbox{havoc(x)}) &=& \{(s,s') \mid OK \rightarrow (OK' \land 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') \} \\ | ||