Differences

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

--- sav07_lecture_3_skeleton [2007/03/20 14:48]
vkuncak
+++ sav07_lecture_3_skeleton [2007/03/20 14:58]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Lecture 3 (Skeleton) ======
+===== Converting programs (with simple values) to formulas =====
 ==== Context ====
@@ Line 6: / Line 10: @@
   * 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
-  * we can represent relations using set comprehensions; if our program r has two state components, we can represent its meaning R(r) as
+  * we can represent relations using set comprehensions; if our program c has two state components, we can represent its meaning R( c ) as
 <latex>
 \{((x_0,y_0),(x,y)) \mid F \}
 </latex>
-    where F is some formula that has x,y,x_0,y_0 as free variables.
+where F is some formula that has x,y,x_0,y_0 as free variables.
-Our goal is to find rules for computing R(r) that are
+  * 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.
+Our goal is to find rules for computing R( c ) that are
   * correct
   * efficient
-  * create formulas that we can prove later
+  * create formulas that we can effectively prove later
+What exactly do we prove about the formula R( c ) ?
+We prove that this formula is **valid**
+  R( c ) -> error=false