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:15]
vkuncak
@@ Line 141: / Line 141: @@
 You can find some example formulas in jahob/examples/nasty_formulas directory of Jahob.
 ==== Language features ====
@@ Line 162: / Line 159: @@
 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,o2,a[i:=o1](i)) = IF(i+k=i+k,o2,a[i:=o1](i+k))
+and then repeating the process we obtain
+  IF(i=i+k,o2,IF(i=i,o1,a(i))) = IF(i+k=i+k,o2,IF(i+k=i,o1,a(i+k)))
+We can in fact simplify some of these expressions and eliminate IF because we know the truth value, 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,o1,a(i)) &
+  v2 = IF(i=i+k,o2,v2) &
+  v3 = IF(i+k=i,o1,a(i+k)) &
+  v4 = IF(i+k=i+k,o2,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,t,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 ====