Add exception declaration, raise, and update logic

Author: lyonel2017

examples/exception.ec

@@ -0,0 +1,206 @@
+require import AllCore.
+
+exception assume.
+exception assert.
+
+module M' ={
+  proc truc (x:int) : int = {
+    raise (x = 3) assume;
+    x <- 1;
+    if (x = 3)  {
+       raise assume;
+    }
+    if (x=3) {
+        raise assert;
+      }
+  return x;
+  }
+}.
+
+print M'.
+
+(* Missing ; after printing raise *)
+
+op p7: bool.
+op p1: bool.
+op p2: bool.
+op p3: bool.
+
+lemma assume_assert :
+hoare [M'.truc : p7 ==> p3 | assume:p1 |assert: p2 ].
+    proof.
+admitted.
+
+op p8: bool.
+op q1: bool.
+op q2: bool.
+op q3: bool.
+
+lemma assert_assume :
+hoare [M'.truc : p8 ==> q3 | assume:q1 |assert: q2 ].
+    proof.
+admitted.
+
+op p4: bool.
+op p5: bool.
+op p6: bool.
+op p9: bool.
+lemma assert_assume' :
+hoare [M'.truc : p9 ==> p4 | assume:p6 |assert: p5 ].
+    proof.
+      conseq (assume_assert) (assert_assume).
+      + admit.
+      + admit.
+    qed.
+
+exception e1.
+exception e2.
+exception e3.
+
+module M ={
+  proc f1 (x:int) : int = {
+    raise (x = 3) e1;
+    x <- 5;
+    return x;
+  }
+
+ proc f2 (x:int) : int = {
+    if (x = 3)  {
+      x <- x;
+      x <@ f1(x);
+    } else {
+      x <@ f1(x);
+    }
+    return x;
+  }
+}.
+
+
+(* Multiple time post for the same exception *)
+
+lemma l_f1 (_x: int):
+hoare [M.f1 : _x = x ==> (4 < res) | e1:_x = 3 | e2: p5 | p4].
+    proof.
+      proc.
+       conseq (: _ ==> x = 5 | e1: _x = 0 | e2: p2 | p3).
+      + admit.
+      + admit.
+    qed.
+
+lemma l_f2 (_x: int):
+hoare [M.f2 : p9 ==> p4 | e1: p2 | e2:p1 | e3: p6 | p1 ].
+    proof.
+      proc.
+      if.
+      + call (: p5 ==> p3 | e1 : p9 | e2: p7 | p8).
+        + admit.
+        admit.
+      call (l_f1 _x).
+      admit.
+  qed.
+
+
+module M1 ={
+    var i:int
+
+  proc f1 (x:int) : int = {
+    i <- 0;
+    raise e2;
+    return x;
+  }
+
+ proc f2 (x:int) : int = {
+      i <- 1;
+      x <@ f1(x);
+      return x;
+  }
+}.
+
+
+lemma test (_x: int):
+hoare [M1.f2 : true ==> true |e2: M1.i = 0].
+ proof.
+   proc.
+   call (: true ==> true | e2 : M1.i = 0).
+   proc.
+   wp. auto.
+ auto.
+qed.
+
+lemma test2 (_x: int):
+hoare [M1.f1 : true ==> true |e2: M1.i = 0].
+    proof.
+      proc.
+           conseq (: _ ==> _ |  e2: M1.i = 0).
+    auto.
+qed.
+
+module M2 ={
+
+  proc f1 (x:int) : int = {
+
+    return x;
+  }
+
+  proc f2 (x:int) : int = {
+    x <- x + 1;
+    x <@ f1(x);
+    return x;
+  }
+}.
+
+
+lemma test3 (_x: int):
+hoare [M2.f1 : _x = x ==> res = _x | e2 : _x = 0].
+proof.
+  proc.
+ auto.
+qed.
+
+lemma test4 (_x: int):
+hoare [M2.f2 : _x = x ==> res = _x + 1 | e2 : _x + 1= 0 ].
+ proof.
+   proc.
+   (* call (test3 (_x )). *)
+   ecall(test3 x).
+   auto.
+qed.
+
+
+
+
+
+
+
+(* module M2 ={ *)
+
+(*   proc f1 (x:int) : int = { *)
+(*     if (x = 0) {raise e2; } *)
+(*     return x; *)
+(*   } *)
+
+(*   proc f2 (x:int) : int = { *)
+(*     x <- x + 1; *)
+(*     x <@ f1(x); *)
+(*     return x; *)
+(*   } *)
+(* }. *)
+
+
+(* lemma test3 (_x: int): *)
+(* hoare [M2.f1 : _x = x ==> res = _x | e2 : _x = 0]. *)
+(* proof. *)
+(*   proc. *)
+(*  auto. *)
+(* qed. *)
+
+(* lemma test4 (_x: int): *)
+(* hoare [M2.f2 : _x = x ==> res = _x + 1 | e2 : _x = 0]. *)
+(*  proof. *)
+(*    proc. *)
+(*    seq 1 : true. *)
+(*    admit. *)
+(*    ecall(test3 x). *)
+(*  auto. *)
+(* qed. *)
+