updated proof sessions

remember to try 'why3 replay' before wasting your time
updating sessions that have been updated
parent 7d060891
......@@ -2,49 +2,50 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="36" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="36" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.5.0" timelimit="36" steplimit="0" memlimit="1000"/>
<file name="../induction.mlw" expanded="true">
<theory name="Hyps" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Induction1" sum="2bc5c8830e0465e3f7ea66559c1c47e3" expanded="true">
<theory name="Induction1" sum="7eea74f3d6205f915272031ec96ea17a" expanded="true">
<goal name="SimpleInduction.base" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="SimpleInduction.induction_step" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="G" expanded="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="Induction2" sum="e02078a7beaa7444ea0c368cdbbaf27a" expanded="true">
<theory name="Induction2" sum="a8f1a215ffc62b6c69c146867532952d" expanded="true">
<goal name="G" expanded="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="LemmaFunction1" sum="1734fa7e58cb56fbbb023240187431f1" expanded="true">
<goal name="WP_parameter ind" expl="VC for ind" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="11"/></proof>
<theory name="LemmaFunction1" sum="39e46ae878545d9212fca324a0adb48d" expanded="true">
<goal name="VC ind" expl="VC for ind" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="G" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</theory>
<theory name="LemmaFunction2" sum="f19bfb27c6ed8a273bbbdbf106c729bd" expanded="true">
<goal name="WP_parameter ind" expl="VC for ind" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="14"/></proof>
<theory name="LemmaFunction2" sum="0905c6df27b097105aca54844f5b2b7d" expanded="true">
<goal name="VC ind" expl="VC for ind" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="G" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</theory>
<theory name="LemmaFunction3" sum="6ed4bf1fe08cfa4f95caf601bc739e85" expanded="true">
<goal name="WP_parameter ind" expl="VC for ind" expanded="true">
<proof prover="2"><result status="valid" time="0.02" steps="22"/></proof>
<theory name="LemmaFunction3" sum="c0775089c12a8bb230c9fd9511ae4803" expanded="true">
<goal name="VC ind" expl="VC for ind" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="51"/></proof>
</goal>
<goal name="G" expanded="true">
<proof prover="2"><result status="valid" time="0.02" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</theory>
</file>
......
......@@ -12,7 +12,7 @@ module InsertionSort
let insertion_sort (a: array int)
ensures { sorted a /\ permut_all (old a) a }
= for i = 1 to length a - 1 do
= "vc:liberal_for" for i = 1 to length a - 1 do
(* a[0..i[ is sorted; now insert a[i] *)
invariant { sorted_sub a 0 i /\ permut_all (old a) a }
let v = a[i] in
......@@ -90,7 +90,7 @@ module InsertionSortGen
let insertion_sort (a: array elt)
ensures { sorted a /\ permut_all (old a) a }
= for i = 1 to length a - 1 do
= "vc:liberal_for" for i = 1 to length a - 1 do
(* a[0..i[ is sorted; now insert a[i] *)
invariant { sorted_sub a 0 i /\ permut_all (old a) a }
let v = a[i] in
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.MinMax.
Require int.ComputerDivision.
Require map.Map.
Require map.Occ.
Require map.MapPermut.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
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]].
(* Why3 assumption *)
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)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
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)) (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) :=
(mk_array n (map.Map.const v: (map.Map.map Z a))).
Axiom elt : Type.
Parameter elt_WhyType : WhyType elt.
Existing Instance elt_WhyType.
Parameter le: elt -> elt -> Prop.
Axiom Refl : forall (x:elt), (le x x).
Axiom Trans : forall (x:elt) (y:elt) (z:elt), (le x y) -> ((le y z) -> (le x
z)).
Axiom Total : forall (x:elt) (y:elt), (le x y) \/ (le y x).
(* Why3 assumption *)
Definition sorted_sub (a:(array elt)) (l:Z) (u:Z): Prop := forall (i1:Z)
(i2:Z), ((l <= i1)%Z /\ ((i1 <= i2)%Z /\ (i2 < u)%Z)) -> (le (get a i1)
(get a i2)).
(* Why3 assumption *)
Definition sorted (a:(array elt)): Prop := forall (i1:Z) (i2:Z),
((0%Z <= i1)%Z /\ ((i1 <= i2)%Z /\ (i2 < (length a))%Z)) -> (le (get a i1)
(get a i2)).
(* Why3 assumption *)
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]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
(* Why3 assumption *)
Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
a)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\
(l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\
(map_eq_sub (elts a1) (elts a2) l u))).
(* Why3 assumption *)
Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub (elts a1) (elts a2)
0%Z (length a1)).
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (l:Z) (u:Z) (i:Z) (j:Z): Prop := ((l <= i)%Z /\
(i < u)%Z) /\ (((l <= j)%Z /\ (j < u)%Z) /\ (((map.Map.get a1
i) = (map.Map.get a2 j)) /\ (((map.Map.get a1 j) = (map.Map.get a2 i)) /\
forall (k:Z), ((l <= k)%Z /\ (k < u)%Z) -> ((~ (k = i)) -> ((~ (k = j)) ->
((map.Map.get a1 k) = (map.Map.get a2 k))))))).
Axiom exchange_set : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)) (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\
(i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> (exchange a1
(map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) l
u i j)).
(* Why3 assumption *)
Definition exchange1 {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\ (exchange (elts a1)
(elts a2) 0%Z (length a1) i j).
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\
(l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\
(map.MapPermut.permut (elts a1) (elts a2) l u))).
(* Why3 assumption *)
Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
(l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((permut a1
a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u (length a1))).
(* Why3 assumption *)
Definition permut_all {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut (elts a1)
(elts a2) 0%Z (length a1)).
Axiom exchange_permut_sub : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (a2:(array a)) (i:Z) (j:Z) (l:Z) (u:Z), (exchange1 a1
a2 i j) -> (((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) ->
((0%Z <= l)%Z -> ((u <= (length a1))%Z -> (permut_sub a1 a2 l u))))).
Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (a2:(array a)) (l1:Z) (u1:Z) (l2:Z) (u2:Z),
(permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) ->
(((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))).
Axiom exchange_permut_all : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (a2:(array a)) (i:Z) (j:Z), (exchange1 a1 a2 i j) ->
(permut_all a1 a2).
(* Why3 goal *)
Theorem WP_parameter_bottom_up_mergesort : forall (a:Z) (a1:(map.Map.map Z
elt)), (0%Z <= a)%Z -> forall (tmp:Z) (tmp1:(map.Map.map Z elt)),
((0%Z <= tmp)%Z /\ ((tmp = a) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < tmp)%Z) -> ((map.Map.get tmp1 i) = (map.Map.get a1 i)))) ->
forall (len:Z) (a2:(map.Map.map Z elt)), let a3 := (mk_array a a2) in
(((1%Z <= len)%Z /\ ((permut_all (mk_array a a1) a3) /\ forall (k:Z),
let l := (k * len)%Z in (((0%Z <= l)%Z /\ (l < a)%Z) -> (sorted_sub a3 l
(ZArith.BinInt.Z.min a (l + len)%Z))))) -> ((len < a)%Z -> forall (i:Z)
(lo:Z) (a4:(map.Map.map Z elt)), let a5 := (mk_array a a4) in
((((0%Z <= lo)%Z /\ (lo = ((2%Z * i)%Z * len)%Z)) /\ ((permut_all a3 a5) /\
((forall (k:Z), let l := (k * len)%Z in (((lo <= l)%Z /\ (l < a)%Z) ->
(sorted_sub a5 l (ZArith.BinInt.Z.min a (l + len)%Z)))) /\ forall (k:Z),
let l := (k * (2%Z * len)%Z)%Z in (((0%Z <= l)%Z /\ (l < lo)%Z) ->
(sorted_sub a5 l (ZArith.BinInt.Z.min a (l + (2%Z * len)%Z)%Z)))))) ->
((~ (lo < (a - len)%Z)%Z) -> ((forall (k:Z), let l :=
(k * (2%Z * len)%Z)%Z in (((0%Z <= l)%Z /\ (l < a)%Z) ->
((l = ((k * 2%Z)%Z * len)%Z) /\ (((l < lo)%Z -> (sorted_sub a5 l
(ZArith.BinInt.Z.min a (l + (2%Z * len)%Z)%Z))) /\ ((lo <= l)%Z ->
((sorted_sub a5 l (ZArith.BinInt.Z.min a (l + len)%Z)) /\
((((ZArith.BinInt.Z.min a (l + (2%Z * len)%Z)%Z) = (ZArith.BinInt.Z.min a (l + len)%Z)) /\
((ZArith.BinInt.Z.min a (l + len)%Z) = a)) /\ (sorted_sub a5 l
(ZArith.BinInt.Z.min a (l + (2%Z * len)%Z)%Z))))))))) -> forall (len1:Z),
(len1 = (2%Z * len)%Z) -> forall (k:Z), let l := (k * len1)%Z in
(((0%Z <= l)%Z /\ (l < a)%Z) -> (sorted_sub a5 l
(ZArith.BinInt.Z.min a (l + len1)%Z)))))))).
intros a a1 h1 tmp tmp1 (h2,(h3,h4)) len a2 a3 (h5,(h6,h7)) h8 i lo a4 a5
((h9,h10),(h11,(h12,h13))) h14 h15 len1 h16 k l (h17,h18).
subst l len1.
destruct (h15 k); clear h15; intuition.
assert (case: (k * (2 * len) < lo \/ lo <= k * (2 * len))%Z) by omega.
destruct case; intuition.
Qed.
This diff is collapsed.
This diff is collapsed.
......@@ -2,91 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.5.0" timelimit="11" steplimit="0" memlimit="1000"/>
<file name="../mjrty.mlw" expanded="true">
<theory name="Mjrty" sum="997a4729c8c41742be81a59084f9c422" expanded="true">
<goal name="WP_parameter mjrty" expl="VC for mjrty" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter mjrty.1" expl="1. index in array bounds">
<proof prover="4" timelimit="5"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter mjrty.2" expl="2. exceptional postcondition">
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter mjrty.3" expl="3. loop invariant init">
<proof prover="4"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter mjrty.4" expl="4. loop invariant init">
<proof prover="4"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter mjrty.5" expl="5. loop invariant init">
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter mjrty.6" expl="6. index in array bounds">
<proof prover="4" timelimit="5"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter mjrty.7" expl="7. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.05" steps="48"/></proof>
</goal>
<goal name="WP_parameter mjrty.8" expl="8. loop invariant preservation">
<proof prover="2" timelimit="5"><result status="valid" time="0.53"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter mjrty.9" expl="9. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter mjrty.10" expl="10. index in array bounds">
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter mjrty.11" expl="11. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.03" steps="32"/></proof>
</goal>
<goal name="WP_parameter mjrty.12" expl="12. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.08" steps="25"/></proof>
</goal>
<goal name="WP_parameter mjrty.13" expl="13. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter mjrty.14" expl="14. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.05" steps="23"/></proof>
</goal>
<goal name="WP_parameter mjrty.15" expl="15. loop invariant preservation">
<proof prover="0" timelimit="30"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter mjrty.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="WP_parameter mjrty.17" expl="17. exceptional postcondition">
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter mjrty.18" expl="18. postcondition">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter mjrty.19" expl="19. exceptional postcondition">
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.03" steps="10"/></proof>
</goal>
<goal name="WP_parameter mjrty.20" expl="20. loop invariant init">
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter mjrty.21" expl="21. index in array bounds">
<proof prover="4" timelimit="5"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter mjrty.22" expl="22. postcondition">
<proof prover="2"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="WP_parameter mjrty.23" expl="23. loop invariant preservation">
<proof prover="4" timelimit="5"><result status="valid" time="0.07" steps="58"/></proof>
</goal>
<goal name="WP_parameter mjrty.24" expl="24. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter mjrty.25" expl="25. exceptional postcondition">
<proof prover="4" memlimit="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
</transf>
<theory name="Mjrty" sum="37ddb792adae0b45a1111bc4d9ae0e24" expanded="true">
<goal name="VC mjrty" expl="VC for mjrty" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,88 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="11" steplimit="0" memlimit="1000"/>
<file name="../muller.mlw" expanded="true">
<theory name="Muller" sum="f9c0e7f73098dd225f02eaeb679d901e" expanded="true">
<goal name="WP_parameter compact" expl="VC for compact" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter compact.1" expl="1. array creation size">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compact.2" expl="2. loop invariant init">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compact.3" expl="3. index in array bounds">
<proof prover="5" timelimit="5" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter compact.4" expl="4. index in array bounds">
<proof prover="4"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter compact.5" expl="5. type invariant">
<proof prover="4"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter compact.6" expl="6. index in array bounds">
<proof prover="4"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="WP_parameter compact.7" expl="7. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
<goal name="WP_parameter compact.8" expl="8. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter compact.9" expl="9. loop invariant init">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compact.10" expl="10. index in array bounds">
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compact.11" expl="11. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.03" steps="30"/></proof>
</goal>
<goal name="WP_parameter compact.12" expl="12. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.04" steps="49"/></proof>
</goal>
<goal name="WP_parameter compact.13" expl="13. array creation size">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compact.14" expl="14. loop invariant init">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter compact.15" expl="15. index in array bounds">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="4" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter compact.16" expl="16. index in array bounds">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter compact.17" expl="17. type invariant">
<proof prover="4"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter compact.18" expl="18. index in array bounds">
<proof prover="4" timelimit="30"><result status="valid" time="15.26" steps="6306"/></proof>
<proof prover="5" timelimit="30" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter compact.19" expl="19. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.03" steps="40"/></proof>
</goal>
<goal name="WP_parameter compact.20" expl="20. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.06" steps="63"/></proof>
</goal>
</transf>
<theory name="Muller" sum="07128ed49e31cb2d58089eca4b67491d" expanded="true">
<goal name="VC compact" expl="VC for compact" expanded="true">
<proof prover="1"><result status="valid" time="0.27" steps="743"/></proof>
</goal>
</theory>
</file>
......
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