From 0f41c425dc345d606f438d0cc3b755fb0fc860cf 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 14:28:36 +0200
Subject: [PATCH] [wp] vset: add new tests for iota
---
src/plugins/wp/tests/wp_acsl/vset.i | 14 ++++++++++++++
1 file changed, 14 insertions(+)
diff --git a/src/plugins/wp/tests/wp_acsl/vset.i b/src/plugins/wp/tests/wp_acsl/vset.i
index 091ba755aab..57820e5ace3 100644
--- a/src/plugins/wp/tests/wp_acsl/vset.i
+++ b/src/plugins/wp/tests/wp_acsl/vset.i
@@ -29,6 +29,19 @@
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);
@@ -37,5 +50,6 @@
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 };
*/
--
GitLab