Commit d56bc53c authored by Andrei Paskevich's avatar Andrei Paskevich

repair some sessions

parent 6af982f1
This diff is collapsed.
......@@ -164,10 +164,10 @@
<proof prover="0" timelimit="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter decompose_back" expl="VC for decompose_back">
<proof prover="1" memlimit="0"><result status="valid" time="0.57"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="WP_parameter front_node" expl="VC for front_node">
<proof prover="0" timelimit="2"><result status="valid" time="1.08"/></proof>
<proof prover="0" timelimit="2"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="WP_parameter front" expl="VC for front">
<proof prover="0" timelimit="2"><result status="valid" time="0.42"/></proof>
......
......@@ -3,9 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../key_type.mlw">
<theory name="KeyType" sum="f40d46a28d2cc72f91f8aae22216ca75">
<theory name="KeyType" sum="a48dcd278fe97312b2055513a393cb02">
</theory>
<theory name="ProgramKeyType" sum="8165294be29fb14ea8c31822cb8616bb">
<theory name="ProgramKeyType" sum="fe9ab2ac91f17434a9491f2c084d35bf">
</theory>
</file>
</why3session>
This diff is collapsed.
......@@ -61,7 +61,7 @@
<proof prover="1" timelimit="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="Sel.WP_parameter avl AVL selected_part" expl="VC for avl AVL selected_part">
<proof prover="1" timelimit="3"><result status="valid" time="0.57"/></proof>
<proof prover="1" timelimit="3"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -116,7 +116,7 @@
<proof prover="1"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter insert" expl="VC for insert">
<proof prover="1"><result status="valid" time="0.78"/></proof>
<proof prover="1"><result status="valid" time="0.58"/></proof>
</goal>
<goal name="WP_parameter remove" expl="VC for remove">
<proof prover="0"><result status="valid" time="0.30"/></proof>
......
......@@ -20,7 +20,7 @@
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter increasing_precede.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.39"/></proof>
<proof prover="0"><result status="valid" time="0.53"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="7" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="7" memlimit="0"/>
<prover id="2" name="Z3" version="2.19" timelimit="5" memlimit="0"/>
<file name="../array_max.mlw" expanded="true">
<theory name="ArrayMax" sum="06ec121fdada4e9dc1a78ddddc222c9c" expanded="true">
<goal name="WP_parameter max" expl="VC for max" expanded="true">
<proof prover="0"><result status="timeout" time="7.00"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="1"><result status="timeout" time="7.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
......
......@@ -8,54 +8,45 @@ Require list.Length.
Require list.Mem.
Require map.Map.
Require list.Append.
Require list.Distinct.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive distinct {a:Type} {a_WT:WhyType a} : (list a) -> Prop :=
| distinct_zero : ((@distinct _ _) nil)
| distinct_one : forall (x:a), ((@distinct _ _) (cons x nil))
| distinct_many : forall (x:a) (l:(list a)), (~ (list.Mem.mem x l)) ->
(((@distinct _ _) l) -> ((@distinct _ _) (cons x l))).
Axiom distinct_append : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)), (distinct l1) -> ((distinct l2) ->
((forall (x:a), (list.Mem.mem x l1) -> ~ (list.Mem.mem x l2)) -> (distinct
(List.app l1 l2)))).
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* 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))).
(* Why3 assumption *)
Inductive tree :=
......@@ -77,10 +68,11 @@ Axiom size_left : forall (t:tree), (0%Z < (size t))%Z -> exists l:tree,
exists r:tree, (t = (Node l r)) /\ ((size l) < (size t))%Z.
(* Why3 assumption *)
Definition all_trees (n:Z) (l:(list tree)): Prop := (distinct l) /\
forall (t:tree), ((size t) = n) <-> (list.Mem.mem t l).
Definition all_trees (n:Z) (l:(list tree)): Prop := (list.Distinct.distinct
l) /\ forall (t:tree), ((size t) = n) <-> (list.Mem.mem t l).
Axiom all_trees_0 : (all_trees 0%Z (cons Empty nil)).
Axiom all_trees_0 : (all_trees 0%Z
(Init.Datatypes.cons Empty Init.Datatypes.nil)).
Axiom tree_diff : forall (l1:tree) (l2:tree), (~ ((size l1) = (size l2))) ->
forall (r1:tree) (r2:tree), ~ ((Node l1 r1) = (Node l2 r2)).
......@@ -88,30 +80,24 @@ Axiom tree_diff : forall (l1:tree) (l2:tree), (~ ((size l1) = (size l2))) ->
(* Why3 goal *)
Theorem WP_parameter_combine : forall (i1:Z) (l1:(list tree)) (i2:Z)
(l2:(list tree)), ((0%Z <= i1)%Z /\ ((all_trees i1 l1) /\ ((0%Z <= i2)%Z /\
(all_trees i2 l2)))) -> forall (l11:(list tree)), (distinct l11) ->
match l11 with
| nil => True
| (cons t1 l12) => forall (l21:(list tree)), (distinct l21) ->
match l21 with
| nil => True
| (cons t2 l22) => (distinct l22) -> forall (o:(list tree)), ((distinct
o) /\ forall (t:tree), (list.Mem.mem t o) <-> exists r:tree,
(t = (Node t1 r)) /\ (list.Mem.mem r l22)) -> forall (t:tree),
(list.Mem.mem t (cons (Node t1 t2) o)) -> exists r:tree,
(t = (Node t1 r)) /\ (list.Mem.mem r l21)
end
end.
(* Why3 intros i1 l1 i2 l2 (h1,(h2,(h3,h4))) l11 h5. *)
intuition.
destruct l11; intuition.
destruct l21; intuition.
unfold Mem.mem in H6; fold @Mem.mem in H6.
destruct H6.
exists t0; intuition.
(all_trees i2 l2)))) -> forall (l11:(list tree)), (list.Distinct.distinct
l11) -> forall (x:tree) (x1:(list tree)),
(l11 = (Init.Datatypes.cons x x1)) -> forall (l21:(list tree)),
(list.Distinct.distinct l21) -> forall (x2:tree) (x3:(list tree)),
(l21 = (Init.Datatypes.cons x2 x3)) -> ((list.Distinct.distinct x3) ->
forall (o:(list tree)), ((list.Distinct.distinct o) /\ forall (t:tree),
(list.Mem.mem t o) <-> exists r:tree, (t = (Node x r)) /\ (list.Mem.mem r
x3)) -> forall (t:tree), (list.Mem.mem t (Init.Datatypes.cons (Node x
x2) o)) -> exists r:tree, (t = (Node x r)) /\ (list.Mem.mem r l21)).
intros i1 l1 i2 l2 (h1,(h2,(h3,h4))) l11 h5 x x1 h6 l21 h7 x2 x3 h8
h9 o (h10,h11) t h12.
subst.
unfold Mem.mem in h12; fold @Mem.mem in h12.
destruct h12.
exists x2; intuition.
red; intuition.
generalize (H8 t1). intuition.
destruct H9 as (r,h); exists r; intuition.
generalize (h11 t). intuition.
destruct H0 as (r,h); exists r; intuition.
red; intuition.
Qed.
This diff is collapsed.
This diff is collapsed.
......@@ -2,16 +2,16 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="0"/>
<prover id="2" name="Vampire" version="0.6" timelimit="5" memlimit="0"/>
<file name="../formula.why">
<theory name="Formula" sum="9bca8ecff9a41b1f5d74310d6cc9d693" expanded="true">
</theory>
<theory name="PropositionalCalculus" sum="357a60841911b7c1403bd2bfc69e5173" expanded="true">
<goal name="Test1" expanded="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
</theory>
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
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