[wp] vset add test oracles

src/plugins/wp/share/why3/frama_c_wp/vset.mlw

@@ -36,7 +36,7 @@ theory Vset
 
   function member_bool 'a (set 'a) : bool
   predicate eqset (a : set 'a) (b : set 'a) =
-    forall x : 'a. (member x a) <-> (member x b)
+    forall x : 'a. (mem x a) <-> (mem x b)
 
   function range int int : set int (* [a..b] *)
   function range_sup int : set int (* [a..] *)
@@ -46,19 +46,19 @@ theory Vset
   (* -------------------------------------------------------------------------- *)
 
   axiom member_bool : forall x:'a. forall s:set 'a [member_bool x s].
-    if member x s then member_bool x s = True else member_bool x s = False
+    if mem x s then member_bool x s = True else member_bool x s = False
 
-  axiom member_range : forall x:int,a:int,b:int [member x (range a b)].
-    member x (range a b) <-> (a <= x /\ x <= b)
+  axiom member_range : forall x:int,a:int,b:int [mem x (range a b)].
+    mem x (range a b) <-> (a <= x /\ x <= b)
 
-  axiom member_range_sup : forall x:int,a:int [member x (range_sup a)].
-    member x (range_sup a) <-> (a <= x)
+  axiom member_range_sup : forall x:int,a:int [mem x (range_sup a)].
+    mem x (range_sup a) <-> (a <= x)
 
-  axiom member_range_inf : forall x:int,b:int [member x (range_inf b)].
-    member x (range_inf b) <-> (x <= b)
+  axiom member_range_inf : forall x:int,b:int [mem x (range_inf b)].
+    mem x (range_inf b) <-> (x <= b)
 
-  axiom member_range_all : forall x:int [member x range_all].
-    member x range_all
+  axiom member_range_all : forall x:int [mem x range_all].
+    mem x range_all
 
   (* -------------------------------------------------------------------------- *)
 

src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle

@@ -19,8 +19,8 @@ Prove: true.
 Goal Lemma 'indirect_equal_constants':
 Assume Lemmas: 'indirect_not_in_constants' 'indirect_in_constants'
   'direct_in_singleton' 'direct_in'
-Prove: member(1, L_Set1) /\ member(2, L_Set1) /\ member(3, L_Set1) /\
-    (forall i : Z. (member(i, L_Set1) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
+Prove: mem(1, L_Set1) /\ mem(2, L_Set1) /\ mem(3, L_Set1) /\
+    (forall i : Z. (mem(i, L_Set1) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
 
 ------------------------------------------------------------
 
@@ -36,8 +36,8 @@ Assume {
   Have: is_sint32(int2_0).
   Have: is_sint32(int3_0).
 }
-Prove: member(int1_0, a) /\ member(int2_0, a) /\ member(int3_0, a) /\
-    (forall i : Z. (member(i, a) ->
+Prove: mem(int1_0, a) /\ mem(int2_0, a) /\ mem(int3_0, a) /\
+    (forall i : Z. (mem(i, a) ->
      ((i = int1_0) \/ (i = int2_0) \/ (i = int3_0)))).
 
 ------------------------------------------------------------
@@ -47,14 +47,14 @@ Assume Lemmas: 'indirect_not_in_logical' 'indirect_in_logical'
   'indirect_not_equal_constants' 'indirect_equal_constants'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
-Prove: member(1, L_Set3) /\ member(2, L_Set3) /\ member(3, L_Set3) /\
-    (forall i : Z. (member(i, L_Set3) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
+Prove: mem(1, L_Set3) /\ mem(2, L_Set3) /\ mem(3, L_Set3) /\
+    (forall i : Z. (mem(i, L_Set3) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
 
 ------------------------------------------------------------
 
 Goal Lemma 'indirect_in_constants':
 Assume Lemmas: 'direct_in_singleton' 'direct_in'
-Prove: member(2, L_Set1).
+Prove: mem(2, L_Set1).
 
 ------------------------------------------------------------
 
@@ -65,7 +65,7 @@ Assume Lemmas: 'indirect_not_equal_logical' 'indirect_equal_logical'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
 Assume { Have: is_sint32(int2_0). }
-Prove: member(int2_0, L_Set2(int3_0, int2_0, int1_0)).
+Prove: mem(int2_0, L_Set2(int3_0, int2_0, int1_0)).
 
 ------------------------------------------------------------
 
@@ -73,16 +73,15 @@ Goal Lemma 'indirect_in_logical':
 Assume Lemmas: 'indirect_not_equal_constants' 'indirect_equal_constants'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
-Prove: member(2, L_Set3).
+Prove: mem(2, L_Set3).
 
 ------------------------------------------------------------
 
 Goal Lemma 'indirect_not_equal_constants':
 Assume Lemmas: 'indirect_equal_constants' 'indirect_not_in_constants'
   'indirect_in_constants' 'direct_in_singleton' 'direct_in'
-Prove: (!member(0, L_Set1)) \/ (!member(1, L_Set1)) \/
-    (!member(2, L_Set1)) \/
-    (exists i : Z. (i != 0) /\ (i != 1) /\ (i != 2) /\ member(i, L_Set1)).
+Prove: (!mem(0, L_Set1)) \/ (!mem(1, L_Set1)) \/ (!mem(2, L_Set1)) \/
+    (exists i : Z. (i != 0) /\ (i != 1) /\ (i != 2) /\ mem(i, L_Set1)).
 
 ------------------------------------------------------------
 
@@ -91,15 +90,14 @@ Assume Lemmas: 'indirect_equal_logical' 'indirect_not_in_logical'
   'indirect_in_logical' 'indirect_not_equal_constants'
   'indirect_equal_constants' 'indirect_not_in_constants'
   'indirect_in_constants' 'direct_in_singleton' 'direct_in'
-Prove: (!member(0, L_Set3)) \/ (!member(1, L_Set3)) \/
-    (!member(2, L_Set3)) \/
-    (exists i : Z. (i != 0) /\ (i != 1) /\ (i != 2) /\ member(i, L_Set3)).
+Prove: (!mem(0, L_Set3)) \/ (!mem(1, L_Set3)) \/ (!mem(2, L_Set3)) \/
+    (exists i : Z. (i != 0) /\ (i != 1) /\ (i != 2) /\ mem(i, L_Set3)).
 
 ------------------------------------------------------------
 
 Goal Lemma 'indirect_not_in_constants':
 Assume Lemmas: 'indirect_in_constants' 'direct_in_singleton' 'direct_in'
-Prove: !member(4, L_Set1).
+Prove: !mem(4, L_Set1).
 
 ------------------------------------------------------------
 
@@ -107,7 +105,7 @@ Goal Lemma 'indirect_not_in_logical':
 Assume Lemmas: 'indirect_in_logical' 'indirect_not_equal_constants'
   'indirect_equal_constants' 'indirect_not_in_constants'
   'indirect_in_constants' 'direct_in_singleton' 'direct_in'
-Prove: !member(0, L_Set3).
+Prove: !mem(0, L_Set3).
 
 ------------------------------------------------------------
 
@@ -118,7 +116,7 @@ Assume Lemmas: 'rec_iota' 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0'
   'indirect_not_equal_constants' 'indirect_equal_constants'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
-Prove: member(0, L_iota(0)).
+Prove: mem(0, L_iota(0)).
 
 ------------------------------------------------------------
 
@@ -132,8 +130,8 @@ Assume Lemmas: 'iota3_compute_equal_constants' 'iota3_compute_2in_constants'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
 Let a = L_iota(1).
-Prove: member(0, a) /\ member(1, a) /\
-    (forall i : Z. (member(i, a) -> ((i = 0) \/ (i = 1)))).
+Prove: mem(0, a) /\ mem(1, a) /\
+    (forall i : Z. (mem(i, a) -> ((i = 0) \/ (i = 1)))).
 
 ------------------------------------------------------------
 
@@ -145,7 +143,7 @@ Assume Lemmas: 'iota0_compute_0in_constants' 'rec_iota' 'rec_iota_gt0'
   'indirect_not_equal_constants' 'indirect_equal_constants'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
-Prove: member(0, L_iota(3)).
+Prove: mem(0, L_iota(3)).
 
 ------------------------------------------------------------
 
@@ -157,7 +155,7 @@ Assume Lemmas: 'iota3_compute_0in_constants' 'iota0_compute_0in_constants'
   'indirect_not_equal_constants' 'indirect_equal_constants'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
-Prove: member(2, L_iota(3)).
+Prove: mem(2, L_iota(3)).
 
 ------------------------------------------------------------
 
@@ -171,9 +169,8 @@ Assume Lemmas: 'iota3_compute_2in_constants' 'iota3_compute_0in_constants'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
 Let a = L_iota(3).
-Prove: member(0, a) /\ member(1, a) /\ member(2, a) /\ member(3, a) /\
-    (forall i : Z. (member(i, a) ->
-     ((i = 0) \/ (i = 1) \/ (i = 2) \/ (i = 3)))).
+Prove: mem(0, a) /\ mem(1, a) /\ mem(2, a) /\ mem(3, a) /\
+    (forall i : Z. (mem(i, a) -> ((i = 0) \/ (i = 1) \/ (i = 2) \/ (i = 3)))).
 
 ------------------------------------------------------------
 
@@ -185,7 +182,7 @@ Assume Lemmas: 'indirect_equal_ghost' 'indirect_in_ghost'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
 Let a = L_iota(n). Assume { Have: n <= 0. }
-Prove: member(0, a) /\ (forall i : Z. (member(i, a) -> (i = 0))).
+Prove: mem(0, a) /\ (forall i : Z. (mem(i, a) -> (i = 0))).
 
 ------------------------------------------------------------
 
@@ -196,8 +193,8 @@ Assume Lemmas: 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0'
   'indirect_not_equal_constants' 'indirect_equal_constants'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
-Assume { Have: member(i, L_iota(n)). }
-Prove: (n = i) \/ member(i, L_iota(n - 1)).
+Assume { Have: mem(i, L_iota(n)). }
+Prove: (n = i) \/ mem(i, L_iota(n - 1)).
 
 ------------------------------------------------------------
 
@@ -208,8 +205,8 @@ Assume Lemmas: 'rec_iota_le0' 'iota_ind0' 'indirect_equal_ghost'
   'indirect_not_equal_constants' 'indirect_equal_constants'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
-Assume { Have: 0 < n. Have: member(i, L_iota(n)). }
-Prove: (n = i) \/ member(i, L_iota(n - 1)).
+Assume { Have: 0 < n. Have: mem(i, L_iota(n)). }
+Prove: (n = i) \/ mem(i, L_iota(n - 1)).
 
 ------------------------------------------------------------
 
@@ -220,7 +217,7 @@ Assume Lemmas: 'iota_ind0' 'indirect_equal_ghost' 'indirect_in_ghost'
   'indirect_not_equal_constants' 'indirect_equal_constants'
   'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
   'direct_in'
-Assume { Have: n <= 0. Have: member(i, L_iota(n)). }
+Assume { Have: n <= 0. Have: mem(i, L_iota(n)). }
 Prove: i = 0.
 
 ------------------------------------------------------------