diff --git a/opam b/opam
index f221a563d28604d800206a45629726462bb97aff..3e99c4d8e557f9f68b9b50f8ffb89125f3521478 100644
--- a/opam
+++ b/opam
@@ -40,6 +40,7 @@ authors: [
"Philippe Herrmann"
"Maxime Jacquemin"
"Florent Kirchner"
+ "Alexander Kogtenkov"
"Tristan Le Gall"
"Jean-Christophe Léchenet"
"Matthieu Lemerre"
diff --git a/src/plugins/gui/help_manager.ml b/src/plugins/gui/help_manager.ml
index 5a9f2a5d04cae97f1fb2b0a96af33e62b3c49efe..9d08557f5be500e6d7a3bfb2bd634388664e8b5f 100644
--- a/src/plugins/gui/help_manager.ml
+++ b/src/plugins/gui/help_manager.ml
@@ -43,6 +43,7 @@ let show main_ui =
"Philippe Herrmann";
"Maxime Jacquemin";
"Florent Kirchner";
+ "Alexander Kogtenkov";
"Tristan Le Gall";
"Jean-Christophe Léchenet";
"Matthieu Lemerre";
diff --git a/src/plugins/wp/share/why3/frama_c_wp/vlist.mlw b/src/plugins/wp/share/why3/frama_c_wp/vlist.mlw
index 838aa45061449c66db8dd2d6ec2a567ee2ce883b..90dd0399e3cdf498d95a0e8fc2d56d4f8ae02fcb 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/vlist.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/vlist.mlw
@@ -28,61 +28,132 @@ theory Vlist
use int.Int
use int.ComputerDivision
+ use list.Append
+ use list.HdTl
+ use list.Nth
+ use option.Option
+
+ use export list.List
+ use export list.Length
(* -------------------------------------------------------------------- *)
(* --- Classical Lists for Alt-Ergo --- *)
(* -------------------------------------------------------------------- *)
- type list 'a
+ function nil : list 'a = Nil
+
+ function cons (x: 'a) (xs: list 'a) : list 'a = Cons x xs
+
+ let function head (l: list 'a) : 'a
+ requires { l <> Nil }
+ ensures { hd l = Some result }
+ = match l with Nil -> absurd | Cons h _ -> h end
+
+ let function tail (l: list 'a) : list 'a
+ requires { l <> Nil }
+ ensures { tl l = Some result }
+ = match l with Nil -> absurd | Cons _ t -> t end
- function nil : list 'a
- function cons 'a (list 'a) : list 'a
- function concat (list 'a) (list 'a) : list 'a
- function repeat (list 'a) int : list 'a
- function length (list 'a) : int
- function nth (list 'a) int : 'a
+ function concat (xs: list 'a) (ys: list 'a) : list 'a = xs ++ ys
function elt (x:'a) : list 'a = cons x nil
+ (* repeat *)
+ (* Here we are forced to use axiomatic definition to conform to ACSL *)
+
+ function repeat (xs: list 'a) (n: int) : list 'a
+
+ axiom repeat_empty:
+ forall xs : list 'a.
+ repeat xs 0 = Nil
+
+ axiom repeat_pos:
+ forall xs : list 'a, n. n > 0 ->
+ repeat xs n = xs ++ repeat xs (n - 1)
+
+ (* nth *)
+ (* Here we are forced to use axiomatic definition to conform to ACSL *)
+
+ function nth (l: list 'a) (n: int): 'a
+
+ axiom nth_zero:
+ forall l : list 'a, x.
+ nth (Cons x l) 0 = x
+
+ axiom nth_pos:
+ forall l : list 'a, n.
+ l <> Nil -> 0 < n < length l -> nth l n = nth (tail l) (n-1)
+
+ (* -------------------------------------------------------------------- *)
+ (* --- concat --- *)
+ (* -------------------------------------------------------------------- *)
+
+ lemma concat_cons: forall u v: list 'a, x: 'a.
+ concat (cons x u) v = cons x (concat u v)
+
+ let lemma head_concat (u v: list 'a)
+ requires { u <> Nil }
+ ensures { head (concat u v) = head u }
+ = match u with Nil -> absurd | Cons _ _ -> () end
+
+ lemma concat_tail:
+ forall u v: list 'a. u <> Nil -> concat (tail u) v = tail (concat u v)
+
(* -------------------------------------------------------------------- *)
(* --- length --- *)
(* -------------------------------------------------------------------- *)
- axiom length_pos : forall w:list 'a. (Int.(<=) 0 (length w))
+ lemma length_pos : forall w:list 'a. (Int.(<=) 0 (length w))
+
+ lemma length_nil : length (nil: list 'a) = 0
- axiom length_nil : length (nil: list 'a) = 0
+ lemma length_nil_bis : forall w:list 'a. length w = 0 -> w = nil
- axiom length_nil_bis : forall w:list 'a. length w = 0 -> w = nil
+ lemma length_not_nil : forall w:list 'a. w <> Nil -> 0 < length w
- axiom length_cons :
+ lemma length_cons :
forall x:'a, w:list 'a [length (cons x w)].
length (cons x w) = (Int.(+) 1 (length w))
- axiom length_concat :
+ lemma length_tail:
+ forall w: list 'a.
+ w <> Nil -> length (tail w) = length w - 1
+
+ lemma singleton_tail: forall w: list 'a. length w = 1 -> tail w = Nil
+
+ lemma length_concat :
forall u,v:list 'a [length (concat u v)].
length (concat u v) = (Int.(+) (length u) (length v))
- axiom length_repeat :
- forall w:list 'a, n:int [length (repeat w n)].
- (Int.(<=) 0 n) -> length (repeat w n) = (Int.( * ) n (length w))
+ let rec lemma length_repeat (w: list 'a) (n: int)
+ requires { 0 <= n }
+ ensures { length (repeat w n) = (Int.( * ) n (length w)) }
+ variant { n }
+ = if 0 < n then length_repeat w (n - 1)
(* -------------------------------------------------------------------- *)
(* --- nth --- *)
(* -------------------------------------------------------------------- *)
- axiom nth_cons:
+ lemma nth_cons:
forall k:int, x:'a, w:list 'a [nth (cons x w) k].
- nth (cons x w) k = if k = 0 then x else nth w (k-1)
+ 0 <= k <= length w -> nth (cons x w) k = if k = 0 then x else nth w (k-1)
+
+ let lemma nth_head (w: list 'a)
+ requires { w <> Nil }
+ ensures { nth w 0 = head w }
+ = match w with Nil -> absurd | Cons _ _ -> () end
- axiom nth_concat:
- forall u,v:list 'a, k:int [nth (concat u v) k].
- nth (concat u v) k = if k < length u then nth u k
- else nth v (Int.(-) k (length u))
+ lemma nth_tail:
+ forall k: int, w: list 'a.
+ 0 < k < length w - 1 -> nth (tail w) (k - 1) = nth w k
- axiom nth_repeat:
- forall n,k:int, w:list 'a [nth (repeat w n) k].
- 0 <= k < (Int.( * ) n (length w)) -> (Int.(<) 0 (length w)) ->
- nth (repeat w n) k = nth w (mod k (length w))
+ let rec lemma nth_concat (u v: list 'a) (k: int)
+ requires { 0 <= k < length u + length v }
+ ensures { nth (concat u v) k =
+ if k < length u then nth u k else nth v (k - length u) }
+ variant { k }
+ = if 0 < k && 0 < length u then nth_concat (tail u) v (k - 1)
(* -------------------------------------------------------------------- *)
(* --- equality of Lists --- *)
@@ -92,8 +163,13 @@ theory Vlist
length u = length v &&
forall i:int. 0 <= i < length u -> nth u i = nth v i
- axiom extensionality:
- forall u,v:list 'a. vlist_eq u v -> u = v
+ let rec lemma extensionality (u v: list 'a)
+ requires { vlist_eq u v }
+ ensures { u = v }
+ variant { length u }
+ = assert { forall x: 'a, r: list 'a. head (cons x r) = x } ;
+ assert { forall x: 'a, r: list 'a. tail (cons x r) = r } ;
+ match u, v with Cons _ x, Cons _ y -> extensionality x y | _ -> () end
(* -------------------------------------------------------------------- *)
(* --- neutral elements --- *)
@@ -101,7 +177,6 @@ theory Vlist
lemma eq_nil_concat:
forall w:list 'a. vlist_eq (concat nil w) w /\ vlist_eq (concat w nil) w
- meta "remove_for_" lemma eq_nil_concat
lemma rw_nil_concat_left:
forall w:list 'a [concat nil w]. concat nil w = w
@@ -114,28 +189,24 @@ theory Vlist
(* -------------------------------------------------------------------- *)
lemma eq_cons_concat:
- forall x:'a, v,w:list 'a [concat (cons x v) w].
+ forall x:'a, v,w:list 'a [concat (cons x v) w].
vlist_eq (concat (cons x v) w) (cons x (concat v w))
- meta "remove_for_" lemma eq_cons_concat
lemma rw_cons_concat:
forall x:'a, v,w:list 'a [concat (cons x v) w].
(concat (cons x v) w) = (cons x (concat v w))
- meta "remove_for_" lemma rw_cons_concat
lemma rw_nil_cons_concat:
forall x:'a, w:list 'a [concat (cons x nil) w].
(concat (cons x nil) w) = (cons x w)
- meta "remove_for_" lemma rw_nil_cons_concat
(* -------------------------------------------------------------------- *)
(* --- associativity --- *)
(* -------------------------------------------------------------------- *)
- lemma eq_assoc_concat:
+ lemma eq_assoc_concat:
forall u,v,w:list 'a.
vlist_eq (concat (concat u v) w) (concat u (concat v w))
- meta "remove_for_" lemma eq_assoc_concat
(* -------------------------------------------------------------------- *)
(* --- repeat --- *)
@@ -149,53 +220,76 @@ theory Vlist
forall w:list 'a [repeat w 0].
repeat w 0 = nil
- lemma eq_repeat_one:
- forall w:list 'a. vlist_eq (repeat w 1) w
- meta "remove_for_" lemma eq_repeat_one
+ let lemma eq_repeat_one (w: list 'a)
+ ensures { vlist_eq (repeat w 1) w }
+ = assert { repeat w 1 = repeat w 0 ++ w }
lemma rw_repeat_one:
forall w:list 'a [repeat w 1]. repeat w 1 = w
+ let rec lemma repeat_more (w: list 'a) (n: int)
+ requires { 0 <= n }
+ ensures { repeat w (n + 1) = concat (repeat w n) w }
+ variant { n }
+ = if 0 < n then repeat_more w (n - 1)
+
+ let rec lemma rw_repeat_concat (p q: int) (w: list 'a)
+ requires { 0 <= p }
+ requires { 0 <= q }
+ ensures { repeat w (Int.(+) p q) = concat (repeat w p) (repeat w q) }
+ variant { p }
+ = if 0 < p then rw_repeat_concat (p - 1) q w
+
lemma eq_repeat_concat:
forall p,q:int, w:list 'a.
0 <= p -> 0 <= q ->
vlist_eq (repeat w (Int.(+) p q)) (concat (repeat w p) (repeat w q))
- meta "remove_for_" lemma eq_repeat_concat
-
- lemma rw_repeat_concat:
- forall p,q:int, w:list 'a.
- 0 <= p -> 0 <= q ->
- repeat w (Int.(+) p q) = concat (repeat w p) (repeat w q)
- meta "remove_for_" lemma rw_repeat_concat
lemma rw_repeat_after:
forall p:int, w:list 'a.
0 <= p -> concat (repeat w p) w = repeat w (Int.(+) p 1)
- meta "remove_for_" lemma rw_repeat_after
lemma rw_repeat_before:
forall p:int, w:list 'a.
0 <= p -> concat w (repeat w p) = repeat w (Int.(+) p 1)
- meta "remove_for_" lemma rw_repeat_before
+
+ let rec lemma nth_repeat (w: list 'a) (n k: int)
+ requires { 0 <= k < n * length w }
+ ensures { nth (repeat w n) k = nth w (mod k (length w)) }
+ variant { n }
+ =
+ if n <= 0 then absurd
+ else if n = 1 then ()
+ else
+ if k < length w
+ then begin
+ assert { (n - 1) * length w >= 1 * length w };
+ nth_repeat w (n - 1) k
+ end
+ else begin
+ let lw = length w in
+ nth_repeat w (n - 1) (k - lw);
+ assert { mod (lw * 1 + (k - lw)) lw = mod (k - lw) lw };
+ end
(*--- To avoid exponential blowup of use of repeat_after by alt-ergo ---*)
-function repeat_box (list 'a) int : (list 'a) (* repeat *)
+ function repeat_box (list 'a) int : (list 'a) (* repeat *)
-axiom rw_repeat_box_unfold:
- forall w:list 'a, n:int [ repeat_box w n ].
- repeat_box w n = repeat w n
+ axiom rw_repeat_box_unfold:
+ forall w:list 'a, n:int [ repeat_box w n ].
+ repeat_box w n = repeat w n
-axiom rw_repeat_plus_box_unfold:
- forall w:list 'a, a,b: int [ repeat_box w (Int.(+) a b) ].
- (Int.(<=) 0 a)
- -> (Int.(<=) 0 b)
- -> repeat_box w (Int.(+) a b) = concat (repeat w a)
+ axiom rw_repeat_plus_box_unfold:
+ forall w:list 'a, a,b: int [ repeat_box w (Int.(+) a b) ].
+ (Int.(<=) 0 a)
+ -> (Int.(<=) 0 b)
+ -> repeat_box w (Int.(+) a b) = concat (repeat w a)
(repeat w b)
-axiom rw_repeat_plus_one_box_unfold:
- forall w:list 'a, n:int [ repeat_box w n ].
- (Int.(<) 0 n)
- -> (repeat_box w n = (concat (repeat w (Int.(-) n 1)) w)
- && (repeat_box w (Int.(+) n 1) = concat (repeat w n) w))
+ axiom rw_repeat_plus_one_box_unfold:
+ forall w:list 'a, n:int [ repeat_box w n ].
+ (Int.(<) 0 n)
+ -> (repeat_box w n = (concat (repeat w (Int.(-) n 1)) w)
+ && (repeat_box w (Int.(+) n 1) = concat (repeat w n) w))
end
diff --git a/src/plugins/wp/tests/wp_plugin/nth.i b/src/plugins/wp/tests/wp_plugin/nth.i
index 33236ef838299d9fff8a9616d03b62b76f261b9c..88491366a5ba6dc6e2092f577d26e26635d20578 100644
--- a/src/plugins/wp/tests/wp_plugin/nth.i
+++ b/src/plugins/wp/tests/wp_plugin/nth.i
@@ -83,14 +83,16 @@
check lemma nth_repeat_3: ok: \nth ( ([| f(0), f(1), f(2), f(3) |] *^ 3) ^ [| f(12) |] , 12 ) == f(12);
check lemma nth_repeat_4: ok: \nth ( ([| f(0), f(1), f(2), f(3) |] *^ 3) ^ [| f(12),f(13),f(14)|] ^ S, 13 ) == f(13);
- lemma access_16_16: ok:
- \forall integer k ; 0 <= k < 16 ==>
- f(k)==\nth([| f(0), f(1), f(2), f(3), f(4), f(5), f(6), f(7),
- f(8), f(9), f(10), f(11), f(12), f(13), f(14), f(15) |], k);
lemma access_4_4: ok:
\forall integer k ; 0 <= k < 4 ==>
- f(k)==\nth([| f(0), f(1), f(2), f(3) |], k);
+ f(k)==\nth([| f(0), f(1), f(2), f(3) |], k);
+
+ // Performance problem with Alt-Ergo, cvc4 & z3 are ok.
+ lemma access_8_8: ko:
+ \forall integer k ; 0 <= k < 6 ==>
+ f(k)==\nth([| f(0), f(1), f(2), f(3),
+ f(4), f(5), f(6), f(7) |], k);
lemma eq_repeat_concat_3: ok: (S *^ 3) == (S ^ S ^ S) ;
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
index c93629cbb62d4b5fa92e4144cc23d6e0c1089cf1..3042f600a4b71ccf48ac6ebb5e178b17fd97c225 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
@@ -96,35 +96,33 @@ Prove: true
Axiomatic 'Nth'
------------------------------------------------------------
-Lemma access_16_16:
-Prove: (0<=k_0) -> (k_0<=15)
+Lemma access_4_4:
+Prove: (0<=k_0) -> (k_0<=3)
-> ((nth
- (concat (elt (L_f 0)) (elt (L_f 1)) (elt (L_f 2)) (elt (L_f 3))
- (elt (L_f 4)) (elt (L_f 5)) (elt (L_f 6)) (elt (L_f 7))
- (elt (L_f 8)) (elt (L_f 9)) (elt (L_f 10)) (elt (L_f 11))
- (elt (L_f 12)) (elt (L_f 13)) (elt (L_f 14)) (elt (L_f 15)))
+ (concat (elt (L_f 0)) (elt (L_f 1)) (elt (L_f 2)) (elt (L_f 3)))
k_0)=(L_f k_0))
------------------------------------------------------------
-Lemma access_4_4:
-Assume: 'access_16_16'
-Prove: (0<=k_0) -> (k_0<=3)
+Lemma access_8_8:
+Assume: 'access_4_4'
+Prove: (0<=k_0) -> (k_0<=5)
-> ((nth
- (concat (elt (L_f 0)) (elt (L_f 1)) (elt (L_f 2)) (elt (L_f 3)))
- k_0)=(L_f k_0))
+ (concat (elt (L_f 0)) (elt (L_f 1)) (elt (L_f 2)) (elt (L_f 3))
+ (elt (L_f 4)) (elt (L_f 5)) (elt (L_f 6)) (elt (L_f 7))) k_0)=
+ (L_f k_0))
------------------------------------------------------------
Lemma access_repeat_concat_3:
-Assume: 'eq_repeat_concat_3' 'access_4_4' 'access_16_16'
+Assume: 'eq_repeat_concat_3' 'access_8_8' 'access_4_4'
Prove: (0<=k_0) -> (k_0<(3*(length L_S)))
-> ((nth (concat L_S L_S L_S) k_0)=(nth (repeat L_S 3) k_0))
------------------------------------------------------------
Lemma eq_repeat_concat_3:
-Assume: 'access_4_4' 'access_16_16'
+Assume: 'access_8_8' 'access_4_4'
Prove: true
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
index 1aeb2e63b01db6747367dd9c88cba0399224c93d..edb9844f6a4b1a158e205f172e3bd85ea2241b20 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
@@ -2,8 +2,8 @@
[kernel] Parsing nth.i (no preprocessing)
[wp] Running WP plugin...
[wp] 26 goals scheduled
-[wp] [Valid] typed_lemma_access_16_16_ok (Alt-Ergo) (Cached)
[wp] [Valid] typed_lemma_access_4_4_ok (Alt-Ergo) (Cached)
+[wp] [Unsuccess] typed_lemma_access_8_8_ko (Alt-Ergo) (Cached)
[wp] [Valid] typed_lemma_access_repeat_concat_3_ok_lack (Alt-Ergo) (Cached)
[wp] [Valid] typed_check_lemma_constructor_elt_ok (Qed)
[wp] [Valid] typed_lemma_eq_repeat_concat_3_ok (Qed)
@@ -28,13 +28,13 @@
[wp] [Valid] typed_check_lemma_right_unfold_repeat1_ok (Qed)
[wp] [Valid] typed_check_lemma_right_unfold_repeat2_ok (Qed)
[wp] [Valid] typed_check_lemma_subsequence1_ok (Qed)
-[wp] Proved goals: 25 / 26
+[wp] Proved goals: 24 / 26
Qed: 22
- Alt-Ergo: 3
- Unsuccess: 1
+ Alt-Ergo: 2
+ Unsuccess: 2
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic Equality 13 - 13 100%
Axiomatic MkRepeat 4 - 4 100%
- Axiomatic Nth 5 3 9 88.9%
+ Axiomatic Nth 5 2 9 77.8%
------------------------------------------------------------