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_lecture_2 [2007/03/22 20:35]
vkuncak
sav07_lecture_2 [2007/04/03 20:31]
kremena.diatchka
Line 248: Line 248:
  
 What is a formal proof? What is a formal proof?
 +
  
  
Line 308: Line 309:
 \end{equation*} \end{equation*}
  
-Sets and properties ​are interchangable.+Sets and predicates ​are interchangable.
  
 $x \in P$ turns set into predicate. $x \in P$ turns set into predicate.
Line 371: Line 372:
 <​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 506:
  
 Weakest preconditions of assignments make wp very appealing. Weakest preconditions of assignments make wp very appealing.
- 
- 
- 
- 
- 
- 
- 
- 
- 
-