Differences

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

--- sav08:backward_vcg_with_loops [2008/03/05 01:41]
vkuncak created
+++ sav08:backward_vcg_with_loops [2009/03/11 10:58]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Backward VCG with Loops ======
-  * [[http://research.microsoft.com/~leino/papers/krml157.pdf|Weakest preconditions for unstructured programs]]
+When using wp, we do not need to separately accumulate verification conditions, because we accumulate them all in the precondition formula.
+===== Desugaring loops with loop invariants ====
+The following transformation is used in ESC/Java and Spec# to check loops with supplied loop invariants.
+while [inv I] (F) c1
+ =>
+  assert(I);
+  havoc(x1,...,xn);    (those that can be modified in the loop)
+  assume(I);
+  assume(~F);
+Provided that I is inductive.  We can check that I is inductive by proving:
+  assume(I);
+  assume(F);
+  c1;
+  assert(I);
+in isolation.  Or proving
+  havoc(x1,...,xn)
+  assume(I);
+  assume(F);
+  c1;
+  assert(I);
+at any point.  If we combine these two, we get:
+ =>
+  assert(I);
+  havoc(x1,...,xn);
+  assume(I);
+   (assume(~F) []
+    assume(F);
+    c1;
+    assert I;
+    assume(false));
+Benefit: if there is x_{n+1} that is not changed, we do not need to write its properties in the loop invariant.  This can make loop invariant shorter.
+===== Avoiding Exponential Explosion =====
+The tricks to avoid exponential explosion can also be implemented in backwards verification-condition generation, using a variant of static single assignment form.
   * [[http://doi.acm.org/10.1145/360204.360220|Avoiding exponential explosion: generating compact verification conditions]]
+  * [[http://research.microsoft.com/~leino/papers/krml157.pdf|Weakest preconditions for unstructured programs]]
+  * [[http://citeseer.ist.psu.edu/697165.html|Efficient weakest preconditions]]