Commit 9ddbd8d7 authored by MARCHE Claude's avatar MARCHE Claude

Update sessions: enforce Alt-Ergo 0.95.2 in some use of why3 Coq tactic

parent df3b3fe9
......@@ -10,8 +10,8 @@
<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<file name="../dijkstra.mlw">
<theory name="DijkstraShortestPath" sum="afa04af5de17123ae1f4e1a114b65d61">
<file name="../dijkstra.mlw" expanded="true">
<theory name="DijkstraShortestPath" sum="afa04af5de17123ae1f4e1a114b65d61" expanded="true">
<goal name="WP_parameter relax" expl="VC for relax">
<transf name="split_goal_wp">
<goal name="WP_parameter relax.1" expl="1. postcondition">
......@@ -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="12.63"/></proof>
<proof prover="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="11.12"/></proof>
</goal>
</transf>
</goal>
......
(* 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,51 +8,53 @@ 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.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
(mk_array n (map.Map.const v: (map.Map.map Z a))).
Parameter n: Z.
......@@ -64,7 +66,7 @@ Axiom f_prop : forall (k:Z), ((0%Z < k)%Z /\ (k < n)%Z) ->
((0%Z <= (f k))%Z /\ ((f k) < k)%Z).
(* Why3 assumption *)
Inductive path : Z -> Z -> Prop :=
Inductive path: Z -> Z -> Prop :=
| path0 : (path 0%Z 0%Z)
| paths : forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> forall (d:Z) (j:Z),
(path d j) -> ((((f i) <= j)%Z /\ (j < i)%Z) -> (path (d + 1%Z)%Z i)).
......@@ -74,17 +76,17 @@ Definition distance (d:Z) (i:Z): Prop := (path d i) /\ forall (d':Z), (path
d' i) -> (d <= d')%Z.
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
Ltac ae := why3 "Alt-Ergo,0.95.2," timelimit 3.
(* Why3 goal *)
Theorem WP_parameter_distance : let o := n in ((0%Z <= o)%Z ->
(((0%Z < o)%Z \/ (0%Z = o)) -> ((0%Z < o)%Z -> forall (g:(@map.Map.map Z _
Z _)), (((0%Z < o)%Z \/ (0%Z = o)) /\
(g = (map.Map.set (map.Map.const 0%Z:(@map.Map.map Z _ Z _)) 0%Z
(-1%Z)%Z))) -> let o1 := n in ((0%Z <= o1)%Z -> (((0%Z < o1)%Z \/
(0%Z = o1)) -> let o2 := (n - 1%Z)%Z in (((1%Z < o2)%Z \/ (1%Z = o2)) ->
forall (count:Z) (d:(@map.Map.map Z _ Z _)) (g1:(@map.Map.map Z _ Z _)),
((((map.Map.get d 0%Z) = 0%Z) /\ (((map.Map.get g1 0%Z) = (-1%Z)%Z) /\
(((0%Z < o)%Z \/ (0%Z = o)) -> ((0%Z < o)%Z -> forall (g:(map.Map.map Z
Z)), (((0%Z < o)%Z \/ (0%Z = o)) /\
(g = (map.Map.set (map.Map.const 0%Z: (map.Map.map Z Z)) 0%Z (-1%Z)%Z))) ->
let o1 := n in ((0%Z <= o1)%Z -> (((0%Z < o1)%Z \/ (0%Z = o1)) -> let o2 :=
(n - 1%Z)%Z in (((1%Z < o2)%Z \/ (1%Z = o2)) -> forall (count:Z)
(d:(map.Map.map Z Z)) (g1:(map.Map.map Z Z)), ((((map.Map.get d
0%Z) = 0%Z) /\ (((map.Map.get g1 0%Z) = (-1%Z)%Z) /\
(((count + (map.Map.get d
((o2 + 1%Z)%Z - 1%Z)%Z))%Z < ((o2 + 1%Z)%Z - 1%Z)%Z)%Z \/
((count + (map.Map.get d
......
......@@ -92,15 +92,15 @@
<goal name="WP_parameter distance.24" expl="24. assertion">
<proof prover="3" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter distance.25" expl="25. assertion" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="WP_parameter distance.25.1" expl="1. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter distance.25" expl="25. assertion">
<transf name="inline_goal">
<goal name="WP_parameter distance.25.1" expl="1. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter distance.25.1.1" expl="1. assertion">
<proof prover="3" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter distance.25.1.2" expl="2. assertion" expanded="true">
<proof prover="0" edited="distance_Distance_WP_parameter_distance_1.v"><result status="valid" time="3.83"/></proof>
<goal name="WP_parameter distance.25.1.2" expl="2. assertion">
<proof prover="0" edited="distance_Distance_WP_parameter_distance_1.v"><result status="valid" time="5.79"/></proof>
</goal>
</transf>
</goal>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment