From ea4a727a608ccb9f15c08a2e8c4403016bb52143 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Thu, 19 Mar 2015 15:52:43 +0100
Subject: [PATCH] fix session
---
drivers/smt-libv2.drv | 2 +-
...stPath_WP_parameter_shortest_path_code_2.v | 8 +-
...stPath_WP_parameter_shortest_path_code_3.v | 221 +++++++++---------
examples/dijkstra/why3session.xml | 4 +-
4 files changed, 117 insertions(+), 118 deletions(-)
diff --git a/drivers/smt-libv2.drv b/drivers/smt-libv2.drv
index 4a6c55be65..94776df2e9 100644
--- a/drivers/smt-libv2.drv
+++ b/drivers/smt-libv2.drv
@@ -6,7 +6,7 @@ printer "smtv2"
filename "%f-%t-%g.smt2"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
outofmemory "^(error \".*out of memory\")\\|Cannot allocate memory"
-fail "^(error \"\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\)\\(.*\\)\")" "Error: \1"
+fail "^(error \"\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\)\\(.*\\)\")" "Error: \\1"
timeout "interrupted by timeout"
time "why3cpulimit time : %s s"
valid "^unsat"
diff --git a/examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v b/examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v
index 6b3761dc20..fa8e8b9303 100644
--- a/examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v
+++ b/examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v
@@ -203,8 +203,11 @@ Definition inv_succ2 (src:vertex) (s:(set vertex)) (q:(set vertex))
((map.Map.get d y) <= ((map.Map.get d x) + (weight x y))%Z)%Z)).
Require Import Why3.
+Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 5.
+(*
Ltac ae0952 := why3 "Alt-Ergo,0.95.2," timelimit 3.
Ltac z3 := why3 "z3" timelimit 3.
+*)
(* Why3 goal *)
Theorem WP_parameter_shortest_path_code : forall (src:vertex) (dst:vertex),
@@ -266,8 +269,8 @@ intros src dst d (h1,h2) q d1 visited ((h3,h4),h5) q1 d2 visited1
((h24,(h25,(h26,(h27,(h28,(h29,(h30,(h31,h32)))))))),h33) result h34 h35 h36
su1 v1 (h37,h38) q4 d4 h39 v2 h40.
*)
-intuition; try ae0952. (* note Alt-Ergo 0.99.1 solves all ! *)
-
+intuition; try ae.
+(*
destruct (why_decidable_eq v2 v1) as [case|case].
subst v2 d4; rewrite Map.Select_eq.
apply Path_cons.
@@ -285,5 +288,6 @@ z3.
ae0952.
trivial.
ae0952.
+*)
Qed.
diff --git a/examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v b/examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v
index fffb6381bf..10d64143e7 100644
--- a/examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v
+++ b/examples/dijkstra/dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v
@@ -1,4 +1,4 @@
-(* This file is generated by Why3's Coq 8.4 driver *)
+(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
@@ -8,135 +8,133 @@ Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
+Axiom qtmark : Type.
+Parameter qtmark_WhyType : WhyType qtmark.
+Existing Instance qtmark_WhyType.
+
(* Why3 assumption *)
-Inductive ref (a:Type) {a_WT:WhyType a} :=
+Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
-Implicit Arguments mk_ref [[a] [a_WT]].
+Implicit Arguments mk_ref [[a]].
(* Why3 assumption *)
-Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
+Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
-Axiom set : forall (a:Type) {a_WT:WhyType a}, Type.
+Axiom set : forall (a:Type), Type.
Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Existing Instance set_WhyType.
-Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (@set a a_WT) -> Prop.
+Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
(* Why3 assumption *)
-Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(@set a a_WT)) (s2:(@set
- a a_WT)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
+Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
+ a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
-Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
- a a_WT)) (s2:(@set a a_WT)), (infix_eqeq s1 s2) -> (s1 = s2).
+Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+ (s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
-Definition subset {a:Type} {a_WT:WhyType a} (s1:(@set a a_WT)) (s2:(@set
- a a_WT)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
+Definition subset {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
+ a)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
-Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(@set
- a a_WT)), (subset s s).
+Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+ (subset s s).
-Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
- a a_WT)) (s2:(@set a a_WT)) (s3:(@set a a_WT)), (subset s1 s2) -> ((subset
- s2 s3) -> (subset s1 s3)).
+Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+ (s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
+ s3)).
-Parameter empty: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT).
+Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).
(* Why3 assumption *)
-Definition is_empty {a:Type} {a_WT:WhyType a} (s:(@set a a_WT)): Prop :=
+Definition is_empty {a:Type} {a_WT:WhyType a} (s:(set a)): Prop :=
forall (x:a), ~ (mem x s).
-Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(@set
- a a_WT))).
+Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty : (set
+ a))).
Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
- (empty :(@set a a_WT))).
+ (empty : (set a))).
-Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (@set a a_WT) -> (@set
- a a_WT).
+Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
- forall (s:(@set a a_WT)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
+ forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
-Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (@set a a_WT) ->
- (@set a a_WT).
+Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
- (s:(@set a a_WT)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
+ (s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
-Axiom add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(@set
- a a_WT)), (mem x s) -> ((add x (remove x s)) = s).
+Axiom add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
+ a)), (mem x s) -> ((add x (remove x s)) = s).
-Axiom remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(@set
- a a_WT)), ((remove x (add x s)) = (remove x s)).
+Axiom remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
+ a)), ((remove x (add x s)) = (remove x s)).
-Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(@set
- a a_WT)), (subset (remove x s) s).
+Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
+ a)), (subset (remove x s) s).
-Parameter union: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT) -> (@set
- a a_WT) -> (@set a a_WT).
+Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
+ a).
-Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
- a a_WT)) (s2:(@set a a_WT)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/
- (mem x s2)).
+Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+ (s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
-Parameter inter: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT) -> (@set
- a a_WT) -> (@set a a_WT).
+Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
+ a).
-Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
- a a_WT)) (s2:(@set a a_WT)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\
- (mem x s2)).
+Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+ (s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
-Parameter diff: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT) -> (@set
- a a_WT) -> (@set a a_WT).
+Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
+ a).
-Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set a a_WT))
- (s2:(@set a a_WT)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x
- s2)).
+Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+ (s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
-Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
- a a_WT)) (s2:(@set a a_WT)), (subset (diff s1 s2) s1).
+Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+ (s2:(set a)), (subset (diff s1 s2) s1).
-Parameter choose: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT) -> a.
+Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
-Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(@set
- a a_WT)), (~ (is_empty s)) -> (mem (choose s) s).
+Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+ (~ (is_empty s)) -> (mem (choose s) s).
-Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT) -> Z.
+Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.
-Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(@set
- a a_WT)), (0%Z <= (cardinal s))%Z.
+Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+ (0%Z <= (cardinal s))%Z.
-Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(@set
- a a_WT)), ((cardinal s) = 0%Z) <-> (is_empty s).
+Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
+ ((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
- forall (s:(@set a a_WT)), (~ (mem x s)) -> ((cardinal (add x
+ forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x
s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
- forall (s:(@set a a_WT)), (mem x s) ->
- ((cardinal s) = (1%Z + (cardinal (remove x s)))%Z).
+ forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x
+ s)))%Z).
-Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
- a a_WT)) (s2:(@set a a_WT)), (subset s1 s2) ->
- ((cardinal s1) <= (cardinal s2))%Z.
+Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
+ (s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
-Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(@set a a_WT)),
+Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).
Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.
-Parameter v: (@set vertex vertex_WhyType).
+Parameter v: (set vertex).
-Parameter g_succ: vertex -> (@set vertex vertex_WhyType).
+Parameter g_succ: vertex -> (set vertex).
Axiom G_succ_sound : forall (x:vertex), (subset (g_succ x) v).
@@ -145,12 +143,12 @@ Parameter weight: vertex -> vertex -> Z.
Axiom Weight_nonneg : forall (x:vertex) (y:vertex), (0%Z <= (weight x y))%Z.
(* Why3 assumption *)
-Definition min (m:vertex) (q:(@set vertex vertex_WhyType)) (d:(@map.Map.map
- vertex vertex_WhyType Z _)): Prop := (mem m q) /\ forall (x:vertex), (mem x
- q) -> ((map.Map.get d m) <= (map.Map.get d x))%Z.
+Definition min (m:vertex) (q:(set vertex)) (d:(map.Map.map vertex
+ Z)): Prop := (mem m q) /\ forall (x:vertex), (mem x q) -> ((map.Map.get d
+ m) <= (map.Map.get d x))%Z.
(* Why3 assumption *)
-Inductive path : vertex -> vertex -> Z -> Prop :=
+Inductive path: vertex -> vertex -> Z -> Prop :=
| Path_nil : forall (x:vertex), (path x x 0%Z)
| Path_cons : forall (x:vertex) (y:vertex) (z:vertex), forall (d:Z), (path
x y d) -> ((mem z (g_succ y)) -> (path x z (d + (weight y z))%Z)).
@@ -174,42 +172,38 @@ Axiom Main_lemma : forall (src:vertex) (v1:vertex), forall (d:Z), (path src
exists v':vertex, exists d':Z, (shortest_path src v' d') /\ ((mem v1
(g_succ v')) /\ ((d' + (weight v' v1))%Z < d)%Z))).
-Axiom Completeness_lemma : forall (s:(@set vertex vertex_WhyType)),
- (forall (v1:vertex), (mem v1 s) -> forall (w:vertex), (mem w
- (g_succ v1)) -> (mem w s)) -> forall (src:vertex), (mem src s) ->
- forall (dst:vertex), forall (d:Z), (path src dst d) -> (mem dst s).
+Axiom Completeness_lemma : forall (s:(set vertex)), (forall (v1:vertex), (mem
+ v1 s) -> forall (w:vertex), (mem w (g_succ v1)) -> (mem w s)) ->
+ forall (src:vertex), (mem src s) -> forall (dst:vertex), forall (d:Z),
+ (path src dst d) -> (mem dst s).
(* Why3 assumption *)
-Definition inv_src (src:vertex) (s:(@set vertex vertex_WhyType)) (q:(@set
- vertex vertex_WhyType)): Prop := (mem src s) \/ (mem src q).
+Definition inv_src (src:vertex) (s:(set vertex)) (q:(set vertex)): Prop :=
+ (mem src s) \/ (mem src q).
(* Why3 assumption *)
-Definition inv (src:vertex) (s:(@set vertex vertex_WhyType)) (q:(@set
- vertex vertex_WhyType)) (d:(@map.Map.map vertex vertex_WhyType
- Z _)): Prop := (inv_src src s q) /\ (((map.Map.get d src) = 0%Z) /\
+Definition inv (src:vertex) (s:(set vertex)) (q:(set vertex)) (d:(map.Map.map
+ vertex Z)): Prop := (inv_src src s q) /\ (((map.Map.get d src) = 0%Z) /\
((subset s v) /\ ((subset q v) /\ ((forall (v1:vertex), (mem v1 q) ->
~ (mem v1 s)) /\ ((forall (v1:vertex), (mem v1 s) -> (shortest_path src v1
(map.Map.get d v1))) /\ forall (v1:vertex), (mem v1 q) -> (path src v1
(map.Map.get d v1))))))).
(* Why3 assumption *)
-Definition inv_succ (src:vertex) (s:(@set vertex vertex_WhyType)) (q:(@set
- vertex vertex_WhyType)) (d:(@map.Map.map vertex vertex_WhyType
- Z _)): Prop := forall (x:vertex), (mem x s) -> forall (y:vertex), (mem y
- (g_succ x)) -> (((mem y s) \/ (mem y q)) /\ ((map.Map.get d
- y) <= ((map.Map.get d x) + (weight x y))%Z)%Z).
+Definition inv_succ (src:vertex) (s:(set vertex)) (q:(set vertex))
+ (d:(map.Map.map vertex Z)): Prop := forall (x:vertex), (mem x s) ->
+ forall (y:vertex), (mem y (g_succ x)) -> (((mem y s) \/ (mem y q)) /\
+ ((map.Map.get d y) <= ((map.Map.get d x) + (weight x y))%Z)%Z).
(* Why3 assumption *)
-Definition inv_succ2 (src:vertex) (s:(@set vertex vertex_WhyType)) (q:(@set
- vertex vertex_WhyType)) (d:(@map.Map.map vertex vertex_WhyType Z _))
- (u:vertex) (su:(@set vertex vertex_WhyType)): Prop := forall (x:vertex),
- (mem x s) -> forall (y:vertex), (mem y (g_succ x)) -> (((~ (x = u)) \/
- ((x = u) /\ ~ (mem y su))) -> (((mem y s) \/ (mem y q)) /\ ((map.Map.get d
- y) <= ((map.Map.get d x) + (weight x y))%Z)%Z)).
+Definition inv_succ2 (src:vertex) (s:(set vertex)) (q:(set vertex))
+ (d:(map.Map.map vertex Z)) (u:vertex) (su:(set vertex)): Prop :=
+ forall (x:vertex), (mem x s) -> forall (y:vertex), (mem y (g_succ x)) ->
+ (((~ (x = u)) \/ ((x = u) /\ ~ (mem y su))) -> (((mem y s) \/ (mem y q)) /\
+ ((map.Map.get d y) <= ((map.Map.get d x) + (weight x y))%Z)%Z)).
Require Import Why3.
-Ltac ae := why3 "alt-ergo" timelimit 3.
-Ltac z := why3 "z3" timelimit 3.
+Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 10.
Require Import Classical.
Lemma inside_or_exit:
@@ -235,27 +229,27 @@ Qed.
(* Why3 goal *)
Theorem WP_parameter_shortest_path_code : forall (src:vertex) (dst:vertex),
- forall (d:(@map.Map.map vertex vertex_WhyType Z _)), ((mem src v) /\ (mem
- dst v)) -> forall (q:(@set vertex vertex_WhyType)) (d1:(@map.Map.map
- vertex vertex_WhyType Z _)) (visited:(@set vertex vertex_WhyType)),
- ((is_empty visited) /\ ((q = (add src (empty :(@set
- vertex vertex_WhyType)))) /\ (d1 = (map.Map.set d src 0%Z)))) ->
- forall (q1:(@set vertex vertex_WhyType)) (d2:(@map.Map.map
- vertex vertex_WhyType Z _)) (visited1:(@set vertex vertex_WhyType)), ((inv
- src visited1 q1 d2) /\ ((inv_succ src visited1 q1 d2) /\ forall (m:vertex),
- (min m q1 d2) -> forall (x:vertex), forall (dx:Z), (path src x dx) ->
+ forall (d:(map.Map.map vertex Z)), ((mem src v) /\ (mem dst v)) ->
+ forall (q:(set vertex)) (d1:(map.Map.map vertex Z)) (visited:(set vertex)),
+ ((is_empty visited) /\ ((q = (add src (empty : (set vertex)))) /\
+ (d1 = (map.Map.set d src 0%Z)))) -> forall (q1:(set vertex))
+ (d2:(map.Map.map vertex Z)) (visited1:(set vertex)), ((inv src visited1 q1
+ d2) /\ ((inv_succ src visited1 q1 d2) /\ forall (m:vertex), (min m q1
+ d2) -> forall (x:vertex), forall (dx:Z), (path src x dx) ->
((dx < (map.Map.get d2 m))%Z -> (mem x visited1)))) -> forall (o:bool),
((o = true) <-> (is_empty q1)) -> ((~ (o = true)) -> ((~ (is_empty q1)) ->
- forall (q2:(@set vertex vertex_WhyType)), forall (u:vertex), ((min u q1
- d2) /\ (q2 = (remove u q1))) -> ((shortest_path src u (map.Map.get d2
- u)) -> forall (visited2:(@set vertex vertex_WhyType)), (visited2 = (add u
- visited1)) -> forall (su:(@set vertex vertex_WhyType)) (q3:(@set
- vertex vertex_WhyType)) (d3:(@map.Map.map vertex vertex_WhyType Z _)),
+ forall (q2:(set vertex)), forall (u:vertex), ((min u q1 d2) /\
+ (q2 = (remove u q1))) -> ((shortest_path src u (map.Map.get d2 u)) ->
+ forall (visited2:(set vertex)), (visited2 = (add u visited1)) ->
+ forall (su:(set vertex)) (q3:(set vertex)) (d3:(map.Map.map vertex Z)),
((subset su (g_succ u)) /\ ((inv src visited2 q3 d3) /\ (inv_succ2 src
visited2 q3 d3 u su))) -> forall (result:bool), ((result = true) <->
~ (is_empty su)) -> ((~ (result = true)) -> forall (m:vertex), (min m q3
d3) -> forall (x:vertex), forall (dx:Z), (path src x dx) ->
((dx < (map.Map.get d3 m))%Z -> (mem x visited2)))))).
+(* Why3 intros src dst d (h1,h2) q d1 visited (h3,(h4,h5)) q1 d2 visited1
+ (h6,(h7,h8)) o h9 h10 h11 q2 u (h12,h13) h14 visited2 h15 su q3 d3
+ (h16,(h17,h18)) result h19 h20 m h21 x dx h22 h23. *)
intros src dst d (h1,h2) q d1 visited (h3,(h4,h5)) q1 d2 visited1
(h6,(h7,h8)) o h9 h10 h11 q2 u (h12,h13) h14 visited2 h15 su q3 d3
(h16,(h17,h18)) result h19 h20 m h21 x dx h22 h23.
@@ -263,15 +257,16 @@ intros src dst d (h1,h2) q d1 visited (h3,(h4,h5)) q1 d2 visited1
assert (is_empty su) by ae.
clear result h19 h20.
assert (inv_succ src visited2 q3 d3).
- unfold inv_succ. split; z.
+ unfold inv_succ. split; ae.
assert (mem src visited2) by ae.
destruct (inside_or_exit visited2 src x dx); auto.
destruct H2 as (y, (z, (dy, (a1, (a2, (a3, (a4, a5))))))).
unfold min in h21.
-assert (mem z q3) by z.
-assert (Map.get d3 z <= Map.get d3 y + weight y z)%Z by ae.
-assert (dy = Map.get d3 y) by z.
-z.
+assert (mem z q3) by ae.
+assert (Map.get d3 z <= Map.get d3 y + weight y z)%Z
+ by ae.
+assert (dy = Map.get d3 y) by ae.
+ae.
Qed.
diff --git a/examples/dijkstra/why3session.xml b/examples/dijkstra/why3session.xml
index d5170a7cbf..67e9801397 100644
--- a/examples/dijkstra/why3session.xml
+++ b/examples/dijkstra/why3session.xml
@@ -152,7 +152,7 @@
<proof prover="3"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.12.1.7" expl="7.">
- <proof prover="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="11.12"/></proof>
+ <proof prover="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="4.74"/></proof>
</goal>
</transf>
</goal>
@@ -187,7 +187,7 @@
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.17" expl="17. loop invariant preservation">
- <proof prover="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="2.40"/></proof>
+ <proof prover="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="6.55"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.18" expl="18. loop variant decrease">
<proof prover="3"><result status="valid" time="0.07"/></proof>
--
GitLab