Differences

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

--- sav07_lecture_3_skeleton [2007/03/18 19:52]
vkuncak created
+++ 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 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 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)
+Note:
+x=t  is same as  havoc(x);assume(x=t)
+assert false = crash  (stops with error)
+assume true  = skip   (does nothing)
 ==== Papers ====
-* Compact verification conditions using weakest preconditions: http://research.microsoft.com/~leino/papers/krml157.pdf
+  * Verification condition generation in Spec#: http://research.microsoft.com/~leino/papers/krml157.pdf
-* Presburger Arithmetic (PA) bounds: {{papadimitriou81complexityintegerprogramming.pdf}}
+  * Loop invariant inference for set algebra formulas: {{hob-tcs.pdf}}
-* Specializing PA bounds: http://www.lmcs-online.org/ojs/viewarticle.php?id=43&layout=abstract
+  * Induction-iteration method for machine code checking: http://www.cs.wisc.edu/wpis/papers/pldi00.ps
+  * Presburger Arithmetic (PA) bounds: {{papadimitriou81complexityintegerprogramming.pdf}}
+  * Specializing PA bounds: http://www.lmcs-online.org/ojs/viewarticle.php?id=43&layout=abstract