Commit de7a797b authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Updated sessions for easier replay

parent 414a7182
......@@ -239,7 +239,7 @@
<ip_library name="Mark"/>
<ip_qualid name="&apos;mark"/>
</ts_pos>
<ts_pos name="ref" arity="1" id="5368"
<ts_pos name="ref" arity="1" id="5367"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="ref"/>
......@@ -256,247 +256,247 @@
<ip_library name="HighOrd"/>
<ip_qualid name="infix @"/>
</ls_pos>
<ls_pos name="zero" id="307"
<ls_pos name="zero" id="306"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="one" id="308"
<ls_pos name="one" id="307"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="one"/>
</ls_pos>
<ls_pos name="infix &lt;" id="309"
<ls_pos name="infix &lt;" id="308"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &lt;"/>
</ls_pos>
<ls_pos name="infix +" id="1478"
<ls_pos name="infix +" id="1477"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix +"/>
</ls_pos>
<ls_pos name="prefix -" id="1479"
<ls_pos name="prefix -" id="1478"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="prefix -"/>
</ls_pos>
<ls_pos name="infix *" id="1480"
<ls_pos name="infix *" id="1479"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix *"/>
</ls_pos>
<ls_pos name="numof" id="2001"
<ls_pos name="numof" id="2000"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="numof"/>
</ls_pos>
<ls_pos name="get" id="2337"
<ls_pos name="get" id="2336"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="2340"
<ls_pos name="set" id="2339"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="set" id="2787"
<ls_pos name="set" id="2786"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="2829"
<ls_pos name="mixfix [&lt;-]" id="2828"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="sorted_sub" id="3108"
<ls_pos name="sorted_sub" id="3107"
ip_theory="IntArraySorted">
<ip_library name="array"/>
<ip_qualid name="sorted_sub"/>
</ls_pos>
<ls_pos name="sorted" id="3124"
<ls_pos name="sorted" id="3123"
ip_theory="IntArraySorted">
<ip_library name="array"/>
<ip_qualid name="sorted"/>
</ls_pos>
<ls_pos name="k" id="5112" ip_theory="Spec">
<ls_pos name="k" id="5111" ip_theory="Spec">
<ip_qualid name="k"/>
</ls_pos>
<ls_pos name="permut" id="5350"
<ls_pos name="permut" id="5349"
ip_theory="Spec">
<ip_qualid name="permut"/>
</ls_pos>
<ls_pos name="prefix !" id="5374"
<ls_pos name="prefix !" id="5373"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="prefix !"/>
</ls_pos>
<pr_pos name="Assoc" id="1481"
<pr_pos name="Assoc" id="1480"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Unit_def_l" id="1488"
<pr_pos name="Unit_def_l" id="1487"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Unit_def_l"/>
</pr_pos>
<pr_pos name="Unit_def_r" id="1491"
<pr_pos name="Unit_def_r" id="1490"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Unit_def_r"/>
</pr_pos>
<pr_pos name="Inv_def_l" id="1494"
<pr_pos name="Inv_def_l" id="1493"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_l"/>
</pr_pos>
<pr_pos name="Inv_def_r" id="1497"
<pr_pos name="Inv_def_r" id="1496"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_r"/>
</pr_pos>
<pr_pos name="Comm" id="1500"
<pr_pos name="Comm" id="1499"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Assoc" id="1505"
<pr_pos name="Assoc" id="1504"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Assoc"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Mul_distr_l" id="1512"
<pr_pos name="Mul_distr_l" id="1511"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_l"/>
</pr_pos>
<pr_pos name="Mul_distr_r" id="1519"
<pr_pos name="Mul_distr_r" id="1518"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_r"/>
</pr_pos>
<pr_pos name="Comm" id="1537"
<pr_pos name="Comm" id="1536"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Unitary" id="1542"
<pr_pos name="Unitary" id="1541"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Unitary"/>
</pr_pos>
<pr_pos name="NonTrivialRing" id="1545"
<pr_pos name="NonTrivialRing" id="1544"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="NonTrivialRing"/>
</pr_pos>
<pr_pos name="Refl" id="1557"
<pr_pos name="Refl" id="1556"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Refl"/>
</pr_pos>
<pr_pos name="Trans" id="1560"
<pr_pos name="Trans" id="1559"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Trans"/>
</pr_pos>
<pr_pos name="Antisymm" id="1567"
<pr_pos name="Antisymm" id="1566"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Antisymm"/>
</pr_pos>
<pr_pos name="Total" id="1572"
<pr_pos name="Total" id="1571"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Total"/>
</pr_pos>
<pr_pos name="ZeroLessOne" id="1577"
<pr_pos name="ZeroLessOne" id="1576"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="ZeroLessOne"/>
</pr_pos>
<pr_pos name="CompatOrderAdd" id="1578"
<pr_pos name="CompatOrderAdd" id="1577"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderAdd"/>
</pr_pos>
<pr_pos name="CompatOrderMult" id="1585"
<pr_pos name="CompatOrderMult" id="1584"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderMult"/>
</pr_pos>
<pr_pos name="Numof_empty" id="2005"
<pr_pos name="Numof_empty" id="2004"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="Numof_empty"/>
</pr_pos>
<pr_pos name="Numof_right_add" id="2019"
<pr_pos name="Numof_right_add" id="2018"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="Numof_right_add"/>
</pr_pos>
<pr_pos name="Numof_bounds" id="2026"
<pr_pos name="Numof_bounds" id="2025"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="Numof_bounds"/>
</pr_pos>
<pr_pos name="Numof_append" id="2033"
<pr_pos name="Numof_append" id="2032"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="Numof_append"/>
</pr_pos>
<pr_pos name="Numof_left_no_add" id="2042"
<pr_pos name="Numof_left_no_add" id="2041"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="Numof_left_no_add"/>
</pr_pos>
<pr_pos name="Numof_left_add" id="2049"
<pr_pos name="Numof_left_add" id="2048"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="Numof_left_add"/>
</pr_pos>
<pr_pos name="Empty" id="2056"
<pr_pos name="Empty" id="2055"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="Empty"/>
</pr_pos>
<pr_pos name="Full" id="2065"
<pr_pos name="Full" id="2064"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="Full"/>
</pr_pos>
<pr_pos name="numof_increasing" id="2074"
<pr_pos name="numof_increasing" id="2073"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="numof_increasing"/>
</pr_pos>
<pr_pos name="numof_strictly_increasing" id="2083"
<pr_pos name="numof_strictly_increasing" id="2082"
ip_theory="NumOf">
<ip_library name="int"/>
<ip_qualid name="numof_strictly_increasing"/>
</pr_pos>
<pr_pos name="Select_eq" id="2373"
<pr_pos name="Select_eq" id="2372"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="Select_eq"/>
</pr_pos>
<pr_pos name="k_positive" id="5113"
<pr_pos name="k_positive" id="5112"
ip_theory="Spec">
<ip_qualid name="k_positive"/>
</pr_pos>
<pr_pos name="eqlt" id="5345" ip_theory="Spec">
<pr_pos name="eqlt" id="5344" ip_theory="Spec">
<ip_qualid name="eqlt"/>
</pr_pos>
<meta name="remove_logic">
......@@ -505,6 +505,9 @@
<meta name="remove_logic">
<meta_arg_ls id="15"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="306"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="307"/>
</meta>
......@@ -512,7 +515,7 @@
<meta_arg_ls id="308"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="309"/>
<meta_arg_ls id="1477"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1478"/>
......@@ -521,133 +524,130 @@
<meta_arg_ls id="1479"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1480"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2001"/>
<meta_arg_ls id="2000"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2337"/>
<meta_arg_ls id="2336"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2340"/>
<meta_arg_ls id="2339"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2787"/>
<meta_arg_ls id="2786"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2829"/>
<meta_arg_ls id="2828"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3108"/>
<meta_arg_ls id="3107"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3124"/>
<meta_arg_ls id="3123"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="5112"/>
<meta_arg_ls id="5111"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="5350"/>
<meta_arg_ls id="5349"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="5374"/>
<meta_arg_ls id="5373"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1481"/>
<meta_arg_pr id="1480"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1488"/>
<meta_arg_pr id="1487"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1491"/>
<meta_arg_pr id="1490"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1494"/>
<meta_arg_pr id="1493"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1497"/>
<meta_arg_pr id="1496"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1500"/>
<meta_arg_pr id="1499"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1505"/>
<meta_arg_pr id="1504"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1512"/>
<meta_arg_pr id="1511"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1519"/>
<meta_arg_pr id="1518"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1537"/>
<meta_arg_pr id="1536"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1542"/>
<meta_arg_pr id="1541"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1545"/>
<meta_arg_pr id="1544"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1557"/>
<meta_arg_pr id="1556"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1560"/>
<meta_arg_pr id="1559"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1567"/>
<meta_arg_pr id="1566"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1572"/>
<meta_arg_pr id="1571"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1577"/>
<meta_arg_pr id="1576"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1578"/>
<meta_arg_pr id="1577"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1585"/>
<meta_arg_pr id="1584"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2005"/>
<meta_arg_pr id="2004"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2019"/>
<meta_arg_pr id="2018"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2026"/>
<meta_arg_pr id="2025"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2033"/>
<meta_arg_pr id="2032"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2042"/>
<meta_arg_pr id="2041"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2049"/>
<meta_arg_pr id="2048"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2056"/>
<meta_arg_pr id="2055"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2065"/>
<meta_arg_pr id="2064"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2074"/>
<meta_arg_pr id="2073"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2083"/>
<meta_arg_pr id="2082"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2373"/>
<meta_arg_pr id="2372"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="5113"/>
<meta_arg_pr id="5112"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="5345"/>
<meta_arg_pr id="5344"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="2"/>
......@@ -665,7 +665,7 @@
<meta_arg_ts id="64"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="5368"/>
<meta_arg_ts id="5367"/>
</meta>
<goal name="WP_parameter counting_sort.60" expl="60. loop invariant preservation">
<transf name="eliminate_builtin">
......@@ -854,8 +854,8 @@
<proof prover="8" memlimit="1000"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter in_place_counting_sort.41" expl="41. loop invariant init">
<proof prover="3"><result status="valid" time="3.44"/></proof>
<proof prover="9" timelimit="6" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="0" timelimit="10" memlimit="1000"><result status="valid" time="0.22"/></proof>
<proof prover="9" timelimit="10" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter in_place_counting_sort.42" expl="42. loop invariant init">
<proof prover="8" memlimit="1000"><result status="valid" time="0.00" steps="12"/></proof>
......
......@@ -72,8 +72,8 @@ 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,0.95.2," timelimit 5.
Ltac z3 := why3 "Z3,4.3.1," timelimit 5.
Ltac ae := why3 "Alt-Ergo,0.95.2," timelimit 30.
Ltac z3 := why3 "Z3,4.3.1," timelimit 30.
(* Why3 goal *)
Theorem WP_parameter_distance : let o := n in ((0%Z <= o)%Z -> forall (g:Z)
......@@ -102,6 +102,9 @@ Theorem WP_parameter_distance : let o := n in ((0%Z <= o)%Z -> forall (g:Z)
((count < n)%Z -> forall (k:Z), (((0%Z < k)%Z \/ (0%Z = k)) /\
(k < n)%Z) -> forall (d':Z), (path d' k) -> ((map.Map.get d2
k) <= d')%Z))))).
(* Why3 intros o h1 g g1 (h2,(h3,h4)) h5 g2 (h6,h7) o1 h8 d d1 (h9,(h10,h11))
o2 h12 count d2 g3 ((h13,(h14,h15)),(h16,h17)) h18 k (h19,h20) d'
h21. *)
(*
intros o _ _ h3 g _ o1 h4 h5 o2 h6 count d g1 ((h7,(h8,h9)),(h10,h11)) h12 k
(h13,h14) d' h15.
......
......@@ -4,10 +4,10 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="6" name="Coq" version="8.4pl6" timelimit="5" memlimit="1000"/>
<file name="../optimal_replay.mlw" expanded="true">
<theory name="OptimalReplay" sum="4b8a258f2e1b3ac0543c6a100e50f6f8" expanded="true">
<goal name="WP_parameter distance" expl="VC for distance" expanded="true">
......@@ -97,7 +97,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter distance.25.1.2" expl="2. assertion">
<proof prover="2" edited="distance_Distance_WP_parameter_distance_1.v"><result status="valid" time="9.76"/></proof>
<proof prover="6" edited="distance_Distance_WP_parameter_distance_1.v"><result status="valid" time="10.10"/></proof>
</goal>
</transf>
</goal>
......
......@@ -114,7 +114,7 @@
<proof prover="9"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
</theory>
<theory name="SuffixSort" sum="7a7298fc81eebed5a42eb7a0fb5b27c9" expanded="true">
<theory name="SuffixSort" sum="0b9756b7136885e268e47a96f603570a" expanded="true">
<goal name="WP_parameter compare" expl="VC for compare">
<transf name="split_goal_wp">
<goal name="WP_parameter compare.1" expl="1. postcondition">
......@@ -642,8 +642,13 @@
<proof prover="11"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter sort.23" expl="23. loop invariant preservation">
<proof prover="12"><result status="valid" time="2.25" steps="411"/></proof>
<proof prover="13"><result status="valid" time="0.22"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.05"/></proof>
<proof prover="13" timelimit="10"><result status="valid" time="0.22"/></proof>
<transf name="inline_goal">
<goal name="WP_parameter sort.23.1" expl="1. loop invariant preservation">
<proof prover="12" timelimit="10"><result status="valid" time="0.48" steps="150"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sort.24" expl="24. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......
......@@ -2,12 +2,13 @@
<!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.99.1" timelimit="10" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="10" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="10" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="10" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>