add function

examples/hoare_logic/wp2.mlw

@@ -384,6 +384,15 @@ module WP
      ident
      { fresh_in_fmla result q }
 
+  val abstract_effects (i:stmt) (f:fmla) :
+    { }
+    fmla
+    { forall sigma pi sigma' pi':env .
+        eval_fmla sigma pi f /\
+        assigns sigma pi (stmt_writes i) sigma' pi' ->
+        eval_fmla sigma' pi' f
+     }
+
   let rec wp (i:stmt) (q:fmla) =
     { true }
     match i with
@@ -399,9 +408,10 @@ module WP
        (* Fand f q *) (* strict wp, termination required *)
     | Swhile e inv i ->
         Fand inv
-          ((*Fforall*) (Fand
-                     (Fimplies (Fand (Fterm e) inv) (wp i inv))
-                     (Fimplies (Fand (Fnot (Fterm e)) inv) q)))
+          (abstract_effects i
+            (Fand
+                (Fimplies (Fand (Fterm e) inv) (wp i inv))
+                (Fimplies (Fand (Fnot (Fterm e)) inv) q))) 
 
     end
     { valid_triple result i q }