From 5bb5b88294a26f9d7a652f42326d933a3ae07c7b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20Ruet-Cros?= <cecile.ruet-cros@cea.fr>
Date: Wed, 3 Jul 2024 18:03:16 +0200
Subject: [PATCH] [wp] vset: library/test cleanup
---
src/plugins/wp/share/why3/frama_c_wp/vset.mlw | 23 +-
.../wp/tests/wp_acsl/oracle/vset.res.oracle | 212 +++---------------
.../wp_acsl/oracle_qualif/vset.res.oracle | 42 ++--
src/plugins/wp/tests/wp_acsl/vset.i | 53 +----
4 files changed, 71 insertions(+), 259 deletions(-)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
index af94135774d..ee23f283c51 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
@@ -28,6 +28,7 @@ theory Vset
use bool.Bool
use int.Int
+ use map.Map
use export set.Set
(* -------------------------------------------------------------------------- *)
@@ -38,26 +39,32 @@ theory Vset
predicate eqset (a : set 'a) (b : set 'a) =
forall x : 'a. (mem x a) <-> (mem x b)
- function range int int : set int (* [a..b] *)
- function range_sup int : set int (* [a..] *)
- function range_inf int : set int (* [..b] *)
- function range_all : set int (* [..] *)
+ let function range (inf sup:int) : set int (* [a..b] *) =
+ fun elt -> if inf <= elt <= sup then true else false
+
+ function range_sup (sup:int) : set int (* [a..] *) =
+ fun elt -> if elt <= sup then true else false
+
+ function range_inf (inf:int) : set int (* [..b] *) =
+ fun elt -> if inf <= elt then true else false
+
+ function range_all : set int (* [..] *) = fun _ -> true
(* -------------------------------------------------------------------------- *)
axiom member_bool : forall x:'a. forall s:set 'a [member_bool x s].
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 [mem x (range a b)].
+ lemma 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 [mem x (range_sup a)].
+ lemma 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 [mem x (range_inf b)].
+ lemma 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 [mem x range_all].
+ lemma member_range_all : forall x:int [mem x range_all].
mem x range_all
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
index d0bb2c0c3d4..1a1c4a973c9 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
@@ -1,64 +1,47 @@
# frama-c -wp [...]
[kernel] Parsing vset.i (no preprocessing)
[wp] Running WP plugin...
-[wp] 21 goals scheduled
-[wp] [Valid] typed_lemma_direct_in (Qed)
-[wp] [Valid] typed_lemma_direct_in_singleton (Qed)
-[wp] [NoResult] typed_lemma_indirect_in_constants (Qed)
-[wp] [Unsuccess] typed_lemma_indirect_equal_logical (Tactic) (Qed)
-[wp] [Unsuccess] typed_lemma_indirect_equal_ghost (Tactic) (Qed)
-[wp] [Unsuccess] typed_lemma_indirect_equal_constants (Tactic) (Qed)
-[wp] [NoResult] typed_lemma_indirect_not_equal_logical (Qed)
-[wp] [NoResult] typed_lemma_indirect_not_equal_constants (Qed)
-[wp] [NoResult] typed_lemma_indirect_in_logical (Qed)
-[wp] [NoResult] typed_lemma_indirect_in_ghost (Qed)
-[wp] [Unsuccess] typed_lemma_iota1_compute_equal_constants (Tactic) (Qed)
-[wp] [NoResult] typed_lemma_iota0_compute_0in_constants (Qed)
-[wp] [NoResult] typed_lemma_indirect_not_in_logical (Qed)
-[wp] [NoResult] typed_lemma_indirect_not_in_constants (Qed)
-[wp] [Unsuccess] typed_lemma_iota_ind0 (Tactic) (Qed)
-[wp] [Unsuccess] typed_lemma_iota3_compute_equal_constants (Tactic) (Qed)
-[wp] [NoResult] typed_lemma_iota3_compute_2in_constants (Qed)
-[wp] [NoResult] typed_lemma_iota3_compute_0in_constants (Qed)
-[wp] [NoResult] typed_lemma_rec_iota_le0 (Qed)
-[wp] [NoResult] typed_lemma_rec_iota_gt0 (Qed)
-[wp] [NoResult] typed_lemma_rec_iota (Qed)
-[wp] Proved goals: 2 / 21
+[wp] 12 goals scheduled
+[wp] [Valid] typed_check_lemma_direct_in (Qed)
+[wp] [Valid] typed_check_lemma_direct_in_singleton (Qed)
+[wp] [NoResult] typed_check_lemma_indirect_in_constants (Qed)
+[wp] [Unsuccess] typed_check_lemma_indirect_equal_logical (Tactic) (Qed)
+[wp] [Unsuccess] typed_check_lemma_indirect_equal_ghost (Tactic) (Qed)
+[wp] [Unsuccess] typed_check_lemma_indirect_equal_constants (Tactic) (Qed)
+[wp] [NoResult] typed_check_lemma_indirect_not_equal_logical (Qed)
+[wp] [NoResult] typed_check_lemma_indirect_not_equal_constants (Qed)
+[wp] [NoResult] typed_check_lemma_indirect_in_logical (Qed)
+[wp] [NoResult] typed_check_lemma_indirect_in_ghost (Qed)
+[wp] [NoResult] typed_check_lemma_indirect_not_in_logical (Qed)
+[wp] [NoResult] typed_check_lemma_indirect_not_in_constants (Qed)
+[wp] Proved goals: 2 / 12
Qed: 2
- Unsuccess: 19
- Missing: 13
+ Unsuccess: 10
+ Missing: 7
------------------------------------------------------------
Global
------------------------------------------------------------
-Goal Lemma 'direct_in':
+Goal Check Lemma 'direct_in':
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
-Goal Lemma 'direct_in_singleton':
-Assume Lemmas: 'direct_in'
+Goal Check Lemma 'direct_in_singleton':
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
-Goal Lemma 'indirect_equal_constants':
-Assume Lemmas: 'indirect_not_in_constants' 'indirect_in_constants'
- 'direct_in_singleton' 'direct_in'
+Goal Check Lemma 'indirect_equal_constants':
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)))).
Prover Script returns Unsuccess
------------------------------------------------------------
-Goal Lemma 'indirect_equal_ghost':
-Assume Lemmas: 'indirect_in_ghost' 'indirect_not_equal_logical'
- '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'
+Goal Check Lemma 'indirect_equal_ghost':
Let a = L_Set2(int2_0, int1_0).
Assume { Have: is_sint32(int1_0). Have: is_sint32(int2_0). }
Prove: mem(int1_0, a) /\ mem(int2_0, a) /\
@@ -67,186 +50,47 @@ Prover Script returns Unsuccess
------------------------------------------------------------
-Goal Lemma 'indirect_equal_logical':
-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'
+Goal Check Lemma 'indirect_equal_logical':
Prove: mem(1, L_Set3) /\ mem(2, L_Set3) /\
(forall i : Z. (mem(i, L_Set3) -> ((i = 1) \/ (i = 2)))).
Prover Script returns Unsuccess
------------------------------------------------------------
-Goal Lemma 'indirect_in_constants':
-Assume Lemmas: 'direct_in_singleton' 'direct_in'
+Goal Check Lemma 'indirect_in_constants':
Prove: mem(2, L_Set1).
------------------------------------------------------------
-Goal Lemma 'indirect_in_ghost':
-Assume Lemmas: 'indirect_not_equal_logical' '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'
+Goal Check Lemma 'indirect_in_ghost':
Assume { Have: is_sint32(int2_0). }
Prove: mem(int2_0, L_Set2(int2_0, int1_0)).
------------------------------------------------------------
-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'
+Goal Check Lemma 'indirect_in_logical':
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'
+Goal Check Lemma 'indirect_not_equal_constants':
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)).
------------------------------------------------------------
-Goal Lemma 'indirect_not_equal_logical':
-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'
+Goal Check Lemma 'indirect_not_equal_logical':
Prove: (!mem(0, L_Set3)) \/ (!mem(1, L_Set3)) \/
(exists i : Z. (i != 0) /\ (i != 1) /\ mem(i, L_Set3)).
------------------------------------------------------------
-Goal Lemma 'indirect_not_in_constants':
-Assume Lemmas: 'indirect_in_constants' 'direct_in_singleton' 'direct_in'
+Goal Check Lemma 'indirect_not_in_constants':
Prove: !mem(4, L_Set1).
------------------------------------------------------------
-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'
+Goal Check Lemma 'indirect_not_in_logical':
Prove: !mem(0, L_Set3).
------------------------------------------------------------
-
-Goal Lemma 'iota0_compute_0in_constants':
-Assume Lemmas: 'rec_iota' 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0'
- 'indirect_equal_ghost' 'indirect_in_ghost' 'indirect_not_equal_logical'
- '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: mem(0, L_iota(0)).
-
-------------------------------------------------------------
-
-Goal Lemma 'iota1_compute_equal_constants':
-Assume Lemmas: 'iota3_compute_equal_constants' 'iota3_compute_2in_constants'
- 'iota3_compute_0in_constants' 'iota0_compute_0in_constants' 'rec_iota'
- 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0' 'indirect_equal_ghost'
- 'indirect_in_ghost' 'indirect_not_equal_logical' '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'
-Let a = L_iota(1).
-Prove: mem(0, a) /\ mem(1, a) /\
- (forall i : Z. (mem(i, a) -> ((i = 0) \/ (i = 1)))).
-Prover Script returns Unsuccess
-
-------------------------------------------------------------
-
-Goal Lemma 'iota3_compute_0in_constants':
-Assume Lemmas: 'iota0_compute_0in_constants' 'rec_iota' 'rec_iota_gt0'
- 'rec_iota_le0' 'iota_ind0' 'indirect_equal_ghost' 'indirect_in_ghost'
- 'indirect_not_equal_logical' '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: mem(0, L_iota(3)).
-
-------------------------------------------------------------
-
-Goal Lemma 'iota3_compute_2in_constants':
-Assume Lemmas: 'iota3_compute_0in_constants' 'iota0_compute_0in_constants'
- 'rec_iota' 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0' 'indirect_equal_ghost'
- 'indirect_in_ghost' 'indirect_not_equal_logical' '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: mem(2, L_iota(3)).
-
-------------------------------------------------------------
-
-Goal Lemma 'iota3_compute_equal_constants':
-Assume Lemmas: 'iota3_compute_2in_constants' 'iota3_compute_0in_constants'
- 'iota0_compute_0in_constants' 'rec_iota' 'rec_iota_gt0' 'rec_iota_le0'
- 'iota_ind0' 'indirect_equal_ghost' 'indirect_in_ghost'
- 'indirect_not_equal_logical' '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'
-Let a = L_iota(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)))).
-Prover Script returns Unsuccess
-
-------------------------------------------------------------
-
-Goal Lemma 'iota_ind0':
-Assume Lemmas: 'indirect_equal_ghost' 'indirect_in_ghost'
- 'indirect_not_equal_logical' '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'
-Let a = L_iota(n). Assume { Have: n <= 0. }
-Prove: mem(0, a) /\ (forall i : Z. (mem(i, a) -> (i = 0))).
-Prover Script returns Unsuccess
-
-------------------------------------------------------------
-
-Goal Lemma 'rec_iota':
-Assume Lemmas: 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0'
- 'indirect_equal_ghost' 'indirect_in_ghost' 'indirect_not_equal_logical'
- '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'
-Assume { Have: mem(i, L_iota(n)). }
-Prove: (n = i) \/ mem(i, L_iota(n - 1)).
-
-------------------------------------------------------------
-
-Goal Lemma 'rec_iota_gt0':
-Assume Lemmas: 'rec_iota_le0' 'iota_ind0' 'indirect_equal_ghost'
- 'indirect_in_ghost' 'indirect_not_equal_logical' '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'
-Assume { Have: 0 < n. Have: mem(i, L_iota(n)). }
-Prove: (n = i) \/ mem(i, L_iota(n - 1)).
-
-------------------------------------------------------------
-
-Goal Lemma 'rec_iota_le0':
-Assume Lemmas: 'iota_ind0' 'indirect_equal_ghost' 'indirect_in_ghost'
- 'indirect_not_equal_logical' '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'
-Assume { Have: n <= 0. Have: mem(i, L_iota(n)). }
-Prove: i = 0.
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
index 43212023105..389e0d1d4cc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
@@ -1,33 +1,23 @@
# frama-c -wp [...]
[kernel] Parsing vset.i (no preprocessing)
[wp] Running WP plugin...
-[wp] 21 goals scheduled
-[wp] [Valid] typed_lemma_direct_in (Qed)
-[wp] [Valid] typed_lemma_direct_in_singleton (Qed)
-[wp] [Valid] typed_lemma_indirect_equal_constants (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_indirect_equal_ghost (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_indirect_equal_logical (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_indirect_in_constants (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_indirect_in_ghost (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_indirect_in_logical (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_indirect_not_equal_constants (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_indirect_not_equal_logical (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_indirect_not_in_constants (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_indirect_not_in_logical (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_iota0_compute_0in_constants (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_iota1_compute_equal_constants (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_iota3_compute_0in_constants (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_iota3_compute_2in_constants (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_iota3_compute_equal_constants (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_lemma_iota_ind0 (Tactic) (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_rec_iota (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_lemma_rec_iota_gt0 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_rec_iota_le0 (Alt-Ergo) (Cached)
-[wp] Proved goals: 19 / 21
+[wp] 12 goals scheduled
+[wp] [Valid] typed_check_lemma_direct_in (Qed)
+[wp] [Valid] typed_check_lemma_direct_in_singleton (Qed)
+[wp] [Valid] typed_check_lemma_indirect_equal_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_equal_ghost (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_equal_logical (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_in_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_in_ghost (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_in_logical (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_not_equal_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_not_equal_logical (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_not_in_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_indirect_not_in_logical (Alt-Ergo) (Cached)
+[wp] Proved goals: 12 / 12
Qed: 2
- Alt-Ergo: 17
- Unsuccess: 2
+ Alt-Ergo: 10
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Lemma 2 17 21 90.5%
+ Lemma 2 10 12 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/vset.i b/src/plugins/wp/tests/wp_acsl/vset.i
index efe4e4e52c7..8fb1f69586b 100644
--- a/src/plugins/wp/tests/wp_acsl/vset.i
+++ b/src/plugins/wp/tests/wp_acsl/vset.i
@@ -5,55 +5,26 @@
OPT:-wp-auto wp:split
*/
-//@ lemma direct_in: 2 \in {1,2,3};
-//@ lemma direct_in_singleton: 2 \in {2};
+//@ check lemma direct_in: 2 \in {1,2,3};
+//@ check lemma direct_in_singleton: 2 \in {2};
//@ logic set<integer> Set1 = {1,2,3};
-//@ lemma indirect_in_constants: 2 \in Set1;
-//@ lemma indirect_not_in_constants: ! (4 \in Set1);
-//@ lemma indirect_equal_constants: Set1 == {1,2,3};
-//@ lemma indirect_not_equal_constants: Set1 != {0,1,2};
+//@ check lemma indirect_in_constants: 2 \in Set1;
+//@ check lemma indirect_not_in_constants: ! (4 \in Set1);
+//@ check lemma indirect_equal_constants: Set1 == {1,2,3};
+//@ check lemma indirect_not_equal_constants: Set1 != {0,1,2};
//@ logic integer i0 = 0;
//@ logic integer i1 = 1;
//@ logic integer i2 = 2;
//@ logic set<integer> Set3 = {i1,i2};
-//@ lemma indirect_in_logical: i2 \in Set3;
-//@ lemma indirect_not_in_logical: ! (i0 \in Set3);
-//@ lemma indirect_equal_logical: Set3 == {i1,i2};
-//@ lemma indirect_not_equal_logical: Set3 != {i0,i1};
+//@ check lemma indirect_in_logical: i2 \in Set3;
+//@ check lemma indirect_not_in_logical: ! (i0 \in Set3);
+//@ check lemma indirect_equal_logical: Set3 == {i1,i2};
+//@ check lemma indirect_not_equal_logical: Set3 != {i0,i1};
//@ ghost int int1 = 1;
//@ ghost int int2 = 2;
//@ logic set<int> Set2 = {int1,int2};
-//@ lemma indirect_in_ghost: int2 \in Set2;
-//@ lemma indirect_equal_ghost: Set2 == {int1,int2};
-
-/*@
- logic set<integer> iota(integer n) =
- (n <= 0) ? {0} : \union({n}, iota(n-1)) ;
-
- lemma iota_ind0:
- \forall integer n;
- n <= 0 ==> iota(n) == {0};
- lemma rec_iota_le0:
- \forall integer i, n;
- i \in iota(n) ==>
- n <= 0 ==>
- i==0;
- lemma rec_iota_gt0:
- \forall integer i, n;
- i \in iota(n) ==>
- 0 < n ==>
- i==n || i \in iota(n-1);
- lemma rec_iota:
- \forall integer i, n;
- i \in iota(n) ==> i==n || i \in iota(n-1);
-
- lemma iota0_compute_0in_constants: 0 \in iota(0);
- lemma iota3_compute_0in_constants: 0 \in iota(3);
- lemma iota3_compute_2in_constants: 2 \in iota(3);
- lemma iota3_compute_equal_constants: iota(3) == { 0, 1, 2, 3 };
- lemma iota1_compute_equal_constants: iota(1) == { 0, 1 };
-
-*/
+//@ check lemma indirect_in_ghost: int2 \in Set2;
+//@ check lemma indirect_equal_ghost: Set2 == {int1,int2};
--
GitLab