Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav07_homework_4_solution [2007/06/16 21:40] vkuncak |
sav07_homework_4_solution [2007/06/16 21:52] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| This is a sketch of the solution of [[SAV07 Homework 4]] | This is a sketch of the solution of [[SAV07 Homework 4]] | ||
| + | |||
| Line 9: | Line 10: | ||
| R(\mbox{assume}\ F}) &=& \{((x,ok),(x',ok) \mid ok\ \rightarrow\ (F(x) \land x=x' \land ok') \} | R(\mbox{assume}\ F}) &=& \{((x,ok),(x',ok) \mid ok\ \rightarrow\ (F(x) \land x=x' \land ok') \} | ||
| \end{eqnarray*} | \end{eqnarray*} | ||
| + | |||
| + | Then we have | ||
| + | |||
| + | $R(assert(false))=PS^2$. | ||
| + | |||
| + | $R(assume(false))= \{ ((x,ok),(x',ok')) | \lnot ok \}$ | ||
| + | |||
| + | Then we have $R(assert(false)) \circ R(assume(false)) = PS^2 = R(assert(false))$. | ||
| + | |||
| + | Note that we have $R(assume(false)) \circ R(assert(false)) = R(assume(false))$. | ||
| ==== Part 2 ==== | ==== Part 2 ==== | ||