Differences

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

--- sav07_lecture_3_skeleton [2007/03/20 14:10]
vkuncak
+++ sav07_lecture_3_skeleton [2007/03/20 14:27]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Lecture 3 (Skeleton) ======
+==== Context ====
 Recall that we can
   * 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 has two state components, we can represent its meaning as
+  * we can represent relations using set comprehensions; if our program r has two state components, we can represent its meaning R(r) as
 <latex>
 \{((x_0,y_0),(x,y)) \mid F \}
 </latex>
-    where F is some formula that mentions x,y,x_0,y_0.
+    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
+  * correct
+  * efficient
+  * create formulas that we can prove later
+==== Formulas for basic statements ====
+In our simple language, basic statements are assignment, havoc, assume, assert.
+R(x=t) = (x=t & y=y_0 & error=error_0)
+***Note***: all our statements will have the property that if error_0 = true, then error=true.  That is, you can never recover from an error state.  This is convenient: if we prove no errors at the end, then there were never errors in between.
+***Note***: the condition y=y_0 & error=error_0 is called <b>frame condition</b>.  There are as many conjuncts as there are components of the state.  This can be annoying to write, so let us use shorthand frame(x) for it.  The shorthand frame(x) denotes a conjunction of v=v_0 for all v that are distinct from x (in this case y and error).  We can have zero or more variables as arguments of frame, so frame() means that nothing changes.
+R(havoc x) = frame(x)
+R(assume F) = F[x:=x_0, y:=y_0, error:=error_0]
+R(assert F) = (F -> frame)
-Our goal is to compute this formula.
+Note:
+x=t  is same as  havoc(x);assume(x=t)
+assert false = crash  (stops with error)
+assume true  = skip   (does nothing)
 ==== Papers ====