Differences

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

--- sav07_homework_4 [2007/04/18 15:39]
vkuncak
+++ sav07_homework_4 [2007/04/24 22:21]
vkuncak
@@ Line 141: / Line 141: @@
 You can find some example formulas in jahob/examples/nasty_formulas directory of Jahob.
@@ Line 162: / Line 160: @@
 and avoid maintaining the set of allocated objects.
+Here is an example of how you can transform a program into a verification condition.
+Consider a program:
+  j = i + k;
+  a[i] = o1;
+  a[j] = o2;
+  assert (a[i]=a[j]);
+After reducing array assignments to ordinary assignments with update expressions, you obtain:
+  j = i + k;
+  a = a[i:=o1];
+  a = a[j:= o2];
+  assert (a[i]=a[j]);
+Computing weakest precondition with respect to True we get, going backwards, the following formulas:
+  a(i)=a(j)
+  a[j:=o2](i) = a[j:=o2](j)
+  a[i:=o1][j:=o2](i) = a[i:=o1][j:=o2](j)
+  a[i:=o1][i+k:=o2](i) = a[i:=o1][i+k:=o2](i+k)
+This is the formula whose validity we would like to prove.
+To do this, we eliminate array update expressions.  A useful intermediate step is to represent array updates using conditional IF expressions.  After replacing top-level updates the last expression becomes
+  (if i+k=i then o2 else a[i:=o1](i)) = (if i+k=i+k then o2 else a[i:=o1](i+k))
+and then repeating the process we obtain
+  (if i=i+k then o2
+   else (if i=i then o1 else a(i))) =
+  (if i+k=i+k then o2
+   else (if i+k=i then o1 else a(i+k)))
+We can in fact simplify *some* of these 'if' expressions, but this is not necessary, and it is not possible in general.  For example we cannot eliminate if i=i+k ... because we do now know the value of k.
+The solution is therefore to first flatten expressions by introducing fresh variables for all IF expressions and then transform IF expressions into disjunctions and conjunctions.  When proving validity of formulas, we can obtain, for example:
+ (v1 = (if i=i then o1 else a(i))) &
+  v2 = (if i=i+k then o2 else v2) &
+  v3 = (if i+k=i then o1 else a(i+k)) &
+  v4 = (if i+k=i+k then o2 else v3)) --> v2 = v4
+You can generate such formulas by repeatedly extracting the innermost IF expressions and naming them using fresh variables.  If you have such a set of definitions of the form v1=t1, ..., vn=tn then if you are proving validity of formula F you use
+  (v1=t1 & ... & vn=tn) --> F
+As a result, all 'if' expressions occur in formulas of form
+  v = (if c then t else e)
+which you can represent as
+  (c & v=t) | ((not c) & (v = e))
+You can then pretty print such formulas and test their value using formDecider.
 ==== Verifying programs with procedures ====