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/12 16:12] vkuncak |
sav08:assert_and_error_conditions [2009/03/12 16:17] 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 ===== | ||