LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Last revision Both sides next revision
sav07_lecture_2 [2007/03/22 20:35]
vkuncak
sav07_lecture_2 [2007/04/01 17:25]
ghid.maatouk
Line 371: Line 371:
 <​latex>​ <​latex>​
 \begin{array}{l} \begin{array}{l}
-\exists(x_2,​y_2) \{((x_1,​y_1)(x_2,​y_2),​(x_3,​y_3)),​y_2=y_1 \wedge x_2 = x_1 + 3\\+\exists(x_2,​y_2) \{((x_1,​y_1)(x_2,​y_2),​(x_3,​y_3)),​y_2=y_1 \wedge x_2 = y_1 + 3\\
  ​\wedge y_3 = y_2 \wedge x_3 = x_2 + y_2 \}  ​\wedge y_3 = y_2 \wedge x_3 = x_2 + y_2 \}
 \end{array} \end{array}
Line 505: Line 505:
  
 Weakest preconditions of assignments make wp very appealing. Weakest preconditions of assignments make wp very appealing.
- 
- 
- 
- 
- 
- 
- 
- 
- 
-