Differences

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

--- sav07_lecture_3 [2007/03/21 18:51]
yuanjianwz
+++ sav07_lecture_3 [2007/03/22 13:37]
yuanjianwz
@@ Line 136: / Line 136: @@
 Note: when proving our verification condition, instead of proving that semantics of relation implies error=false, it's same as proving that the formula for set sp(U,r) implies error=false, where U is the universal relation, or, in terms of formulas, computing the strongest postcondition of formula 'true'.
@@ Line 150: / Line 152: @@
 We know that the weakest precondition holds following conditions for each relation r and sets Q1, Q2:
   wp(r, Q1 ∧ Q2) = wp(r,Q1) ∧ wp(r,Q2)
-  wp(r, Q1 ∨ Q2) = wp(r,Q1) ∨ wp(r,Q2)
 But for statements, we have:
   wp(Q, x=t) = Q[x:=t]
@@ Line 157: / Line 158: @@
   wp(Q, c1 [] c2) = wp(Q,c1) ∧ wp(Q,c2)
   wp(Q, c1 ; c2) = wp(wp(Q,c2),c1)
+  wp(Q, havoc(x)) = ∀x.Q  (or introduce a fresh variable)
 How to prove: wp(Q,c1 [] c2) = wp(Q,c1) ∧ wp(Q,c2)?
   CR(c1 [] c2) = CR(c1) ∨ CR(c2)
@@ Line 212: / Line 214: @@
 Proof: small model theorem.
 ==== Small model theorem for Quantifier-Free Presburger Arithmetic (QFPA) ====
+The idea is to reduce the case, for example:
+∃x,y,z.F
+reduce to
+∃x≤ M,y≤ M,z ≤ M.F
+We try to figure out M.
+Another example:
+¬t1 < t2
+reduce to
+t2+1≤t1
+How about the not equal ?
+t1≠t2
+can be reduced to
+(t1 < t2 ) ∨ (t2 < t1) => (t1 ≤ t2-1) ∨ (t2 ≤ t1-1)
 First step: transform to disjunctive normal form.