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:35] vkuncak |
sav07_homework_4_solution [2007/06/16 21:40] 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]] | ||
+ | |||
==== Part 1 ==== | ==== Part 1 ==== | ||
\begin{eqnarray*} | \begin{eqnarray*} | ||
- | R(\mbox{havoc x}) &=& \{((x,ok),(x',ok) \mid x,x' \in D \} \\ | + | R(\mbox{havoc x}) &=& \{((x,ok),(x',ok') \mid ok \rightarrow ok' \} \\ |
R(\mbox{assert}\ F}) &=& \{((x,ok),(x',ok') \mid (ok \land F(x)) \rightarrow (x=x' \land ok') \} \\ | R(\mbox{assert}\ F}) &=& \{((x,ok),(x',ok') \mid (ok \land F(x)) \rightarrow (x=x' \land ok') \} \\ | ||
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') \} |