LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav07_homework_4_solution [2007/06/16 21:40]
vkuncak 		sav07_homework_4_solution [2007/06/16 22:12]
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 11:
   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))$.
 +
 +Basically, $R(assert(false))$ and $R(assume(false))$ both act as a left zeros of $\circ$ for the relations of the form $R(c)$. ​
  
 ==== Part 2 ==== ==== Part 2 ====
Line 37: Line 51:
  
 $X \rightarrow Y$: Let $s.c_2 \subseteq G$.  Let $Q = s.c_2$. ​ Then $s.c_2 \subseteq Q$, so also $s.c_1 \subseteq Q$.  Thus $s.c_1 \subseteq s.c_2$. $X \rightarrow Y$: Let $s.c_2 \subseteq G$.  Let $Q = s.c_2$. ​ Then $s.c_2 \subseteq Q$, so also $s.c_1 \subseteq Q$.  Thus $s.c_1 \subseteq s.c_2$.
 +
  
 ==== Part 5 ==== ==== Part 5 ====
 +
 +**Lemma**: $skip;c \equiv c;skip \equiv c$.
  
 $c_1 \sqsubseteq c_2\ \rightarrow\ c_1;c_3 \sqsubseteq c_2;c_3$: $c_1 \sqsubseteq c_2\ \rightarrow\ c_1;c_3 \sqsubseteq c_2;c_3$: