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
Next revision Both sides next revision
sav07_lecture_3_skeleton [2007/03/20 18:16]
wikiadmin 		sav07_lecture_3_skeleton [2007/03/20 21:13]
vkuncak
Line 2: Line 2:
  
 ===== Converting programs (with simple values) to formulas ===== ===== Converting programs (with simple values) to formulas =====
- 
- 
- 
  
  
Line 12: Line 9:
   * represent programs using guarded command language, e.g. desugaring of '​if'​ into non-deterministic choice and assume   * represent programs using guarded command language, e.g. desugaring of '​if'​ into non-deterministic choice and assume
   * give meaning to guarded command language statements as relations   * give meaning to guarded command language statements as relations
-  * we can represent relations using set comprehensions;​ if our program c has two state components, we can represent its meaning R( c ) as  +  * we can represent relations using set comprehensions;​ if our program c has two state components, we can represent its meaning R( c ) as $\{((x_0,​y_0),​(x,​y)) \mid F  \}$, where F is some formula that has x,y,x_0,y_0 as free variables.
- +
-$\{((x_0,​y_0),​(x,​y)) \mid F \}$ +
- +
- +
-, where F is some formula that has x,y,x_0,y_0 as free variables.+
  
   * this is what I mean by ''​simple values'':​ later we will talk about modeling pointers and arrays, but we will still use this as a starting point.   * this is what I mean by ''​simple values'':​ later we will talk about modeling pointers and arrays, but we will still use this as a starting point.
Line 29: Line 21:
 What exactly do we prove about the formula R( c ) ? What exactly do we prove about the formula R( c ) ?
  
-We prove that this formula is **valid**+We prove that this formula is **valid**:
  
   R( c ) -> error=false   R( c ) -> error=false
Line 126: Line 118:
  
  
-Test : \\ 
-\begin{eqnarray*} 
-\Psi_0 &=& -C_{abcd} Y_0^a m^b Y_1^c m^d e^{-2i\gamma} \\ 
-\Psi_4 &=& -C_{abcd} Y_1^a \bar{m}^b Y_1^c \bar{m}^d e^{2i\gamma} 
-\end{eqnarray*}