Commit 13d953d2 authored by MARCHE Claude's avatar MARCHE Claude

updated sessions

parent 264805ac
......@@ -8,18 +8,18 @@
<file name="../add_list.mlw" expanded="true">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="AddListRec" sum="d67dc47228a231353998af4e0d24050a" expanded="true">
<theory name="AddListRec" sum="f062b1e05a91602624b37c4b34762555" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="51"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="49"/></proof>
</goal>
<goal name="WP_parameter main" expl="VC for main" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="AddListImp" sum="a7627a17b1b407f559c2a43c04728e9a" expanded="true">
<theory name="AddListImp" sum="7ac8c0163d88693d0911255c23bfb93d" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
......
......@@ -7,7 +7,7 @@
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Vampire" version="0.6" timelimit="6" memlimit="1000"/>
<file name="../algo63.mlw" expanded="true">
<theory name="Algo63" sum="bdabd47749a2764e643544701257c4e3" expanded="true">
<theory name="Algo63" sum="0097fa1af38060be8e585e2cfc854e2a" expanded="true">
<goal name="WP_parameter exchange" expl="VC for exchange">
<proof prover="2"><result status="valid" time="0.05" steps="31"/></proof>
</goal>
......@@ -491,374 +491,374 @@
<goal name="WP_parameter partition.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="1.39"/></proof>
<metas>
<ts_pos name="ref" arity="1" id="2317"
<ts_pos name="ref" arity="1" id="2315"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="ref"/>
</ts_pos>
<ls_pos name="zero" id="289"
<ls_pos name="zero" id="287"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="one" id="290"
<ls_pos name="one" id="288"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="one"/>
</ls_pos>
<ls_pos name="infix &lt;" id="291"
<ls_pos name="infix &lt;" id="289"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &lt;"/>
</ls_pos>
<ls_pos name="infix &gt;" id="294"
<ls_pos name="infix &gt;" id="292"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &gt;"/>
</ls_pos>
<ls_pos name="infix +" id="1460"
<ls_pos name="infix +" id="1458"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix +"/>
</ls_pos>
<ls_pos name="prefix -" id="1461"
<ls_pos name="prefix -" id="1459"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="prefix -"/>
</ls_pos>
<ls_pos name="infix *" id="1462"
<ls_pos name="infix *" id="1460"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix *"/>
</ls_pos>
<ls_pos name="prefix !" id="2323"
<ls_pos name="prefix !" id="2321"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="prefix !"/>
</ls_pos>
<ls_pos name="get" id="2469"
<ls_pos name="get" id="2467"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="2472"
<ls_pos name="set" id="2470"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="2492"
<ls_pos name="mixfix [&lt;-]" id="2490"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="occ" id="2699"
<ls_pos name="occ" id="2697"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ"/>
</ls_pos>
<ls_pos name="get" id="2904"
<ls_pos name="get" id="2902"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="2919"
<ls_pos name="set" id="2917"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix []" id="2944"
<ls_pos name="mixfix []" id="2942"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="mixfix []"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="2961"
<ls_pos name="mixfix [&lt;-]" id="2959"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="array_eq" id="3327"
<ls_pos name="array_eq" id="3325"
ip_theory="ArrayEq">
<ip_library name="array"/>
<ip_qualid name="array_eq"/>
</ls_pos>
<pr_pos name="Assoc" id="1463"
<pr_pos name="Assoc" id="1461"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Unit_def_l" id="1470"
<pr_pos name="Unit_def_l" id="1468"
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="1473"
<pr_pos name="Unit_def_r" id="1471"
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="1476"
<pr_pos name="Inv_def_l" id="1474"
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="1479"
<pr_pos name="Inv_def_r" id="1477"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_r"/>
</pr_pos>
<pr_pos name="Comm" id="1482"
<pr_pos name="Comm" id="1480"
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="1487"
<pr_pos name="Assoc" id="1485"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Assoc"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Mul_distr_l" id="1494"
<pr_pos name="Mul_distr_l" id="1492"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_l"/>
</pr_pos>
<pr_pos name="Mul_distr_r" id="1501"
<pr_pos name="Mul_distr_r" id="1499"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_r"/>
</pr_pos>
<pr_pos name="Comm" id="1519"
<pr_pos name="Comm" id="1517"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Unitary" id="1524"
<pr_pos name="Unitary" id="1522"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Unitary"/>
</pr_pos>
<pr_pos name="NonTrivialRing" id="1527"
<pr_pos name="NonTrivialRing" id="1525"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="NonTrivialRing"/>
</pr_pos>
<pr_pos name="Refl" id="1539"
<pr_pos name="Refl" id="1537"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Refl"/>
</pr_pos>
<pr_pos name="Trans" id="1542"
<pr_pos name="Trans" id="1540"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Trans"/>
</pr_pos>
<pr_pos name="Antisymm" id="1549"
<pr_pos name="Antisymm" id="1547"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Antisymm"/>
</pr_pos>
<pr_pos name="Total" id="1554"
<pr_pos name="Total" id="1552"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Total"/>
</pr_pos>
<pr_pos name="ZeroLessOne" id="1559"
<pr_pos name="ZeroLessOne" id="1557"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="ZeroLessOne"/>
</pr_pos>
<pr_pos name="CompatOrderMult" id="1567"
<pr_pos name="CompatOrderMult" id="1565"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderMult"/>
</pr_pos>
<pr_pos name="Select_eq" id="2505"
<pr_pos name="Select_eq" id="2503"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="Select_eq"/>
</pr_pos>
<pr_pos name="Select_neq" id="2514"
<pr_pos name="Select_neq" id="2512"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="Select_neq"/>
</pr_pos>
<pr_pos name="exchange_set" id="2605"
<pr_pos name="exchange_set" id="2603"
ip_theory="MapExchange">
<ip_library name="map"/>
<ip_qualid name="exchange_set"/>
</pr_pos>
<pr_pos name="occ_right_no_add" id="2713"
<pr_pos name="occ_right_no_add" id="2711"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_right_no_add"/>
</pr_pos>
<pr_pos name="occ_bounds" id="2731"
<pr_pos name="occ_bounds" id="2729"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_bounds"/>
</pr_pos>
<pr_pos name="occ_append" id="2740"
<pr_pos name="occ_append" id="2738"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_append"/>
</pr_pos>
<pr_pos name="occ_neq" id="2751"
<pr_pos name="occ_neq" id="2749"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_neq"/>
</pr_pos>
<pr_pos name="occ_exists" id="2762"
<pr_pos name="occ_exists" id="2760"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_exists"/>
</pr_pos>
<pr_pos name="occ_pos" id="2773"
<pr_pos name="occ_pos" id="2771"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_pos"/>
</pr_pos>
<meta name="remove_logic">
<meta_arg_ls id="289"/>
<meta_arg_ls id="287"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="290"/>
<meta_arg_ls id="288"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="291"/>
<meta_arg_ls id="289"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="294"/>
<meta_arg_ls id="292"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1460"/>
<meta_arg_ls id="1458"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1461"/>
<meta_arg_ls id="1459"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1462"/>
<meta_arg_ls id="1460"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2323"/>
<meta_arg_ls id="2321"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2469"/>
<meta_arg_ls id="2467"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2472"/>
<meta_arg_ls id="2470"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2492"/>
<meta_arg_ls id="2490"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2699"/>
<meta_arg_ls id="2697"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2904"/>
<meta_arg_ls id="2902"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2919"/>
<meta_arg_ls id="2917"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2944"/>
<meta_arg_ls id="2942"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2961"/>
<meta_arg_ls id="2959"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3327"/>
<meta_arg_ls id="3325"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1463"/>
<meta_arg_pr id="1461"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1470"/>
<meta_arg_pr id="1468"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1473"/>
<meta_arg_pr id="1471"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1476"/>
<meta_arg_pr id="1474"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1479"/>
<meta_arg_pr id="1477"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1482"/>
<meta_arg_pr id="1480"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1487"/>
<meta_arg_pr id="1485"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1494"/>
<meta_arg_pr id="1492"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1501"/>
<meta_arg_pr id="1499"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1519"/>
<meta_arg_pr id="1517"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1524"/>
<meta_arg_pr id="1522"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1527"/>
<meta_arg_pr id="1525"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1539"/>
<meta_arg_pr id="1537"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1542"/>
<meta_arg_pr id="1540"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1549"/>
<meta_arg_pr id="1547"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1554"/>
<meta_arg_pr id="1552"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1559"/>
<meta_arg_pr id="1557"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1567"/>
<meta_arg_pr id="1565"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2505"/>
<meta_arg_pr id="2503"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2514"/>
<meta_arg_pr id="2512"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2605"/>
<meta_arg_pr id="2603"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2713"/>
<meta_arg_pr id="2711"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2731"/>
<meta_arg_pr id="2729"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2740"/>
<meta_arg_pr id="2738"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2751"/>
<meta_arg_pr id="2749"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2762"/>
<meta_arg_pr id="2760"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2773"/>
<meta_arg_pr id="2771"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="2317"/>
<meta_arg_ts id="2315"/>
</meta>
<goal name="WP_parameter partition.4" expl="4. postcondition">
<transf name="eliminate_builtin">
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../algo64.mlw" expanded="true">
<theory name="Algo64" sum="e28f0a9f616adcce7784ce7c284474f0" expanded="true">
<theory name="Algo64" sum="8ab02ef07be464ccc7c31dda9dd33adb" expanded="true">
<goal name="WP_parameter quicksort" expl="VC for quicksort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter quicksort.1" expl="1. precondition">
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../algo65.mlw" expanded="true">
<theory name="Algo65" sum="d8d516c8ad33e7a2736cb548287e47bf" expanded="true">
<theory name="Algo65" sum="83b400a3fbe590385036b24b91ab4989" expanded="true">
<goal name="WP_parameter find" expl="VC for find" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter find.1" expl="1. precondition">
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<file name="../all_distinct.mlw" expanded="true">
<theory name="AllDistinct" sum="7d203083e179a8844f043988072c4161" expanded="true">
<theory name="AllDistinct" sum="3b44ec37df3232d188580bcf31db876f" expanded="true">
<goal name="WP_parameter all_distinct" expl="VC for all_distinct" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter all_distinct.1" expl="1. array creation size" expanded="true">
......
......@@ -6,7 +6,7 @@
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="0"/>
<file name="../arm.mlw" expanded="true">
<theory name="M" sum="d97450a6c255beed8bf40f7d503e79cd" expanded="true">
<theory name="M" sum="0d719c3e6262bb28f7a388d2aa2d5410" expanded="true">
<goal name="WP_parameter insertion_sort" expl="VC for insertion_sort">
<transf name="split_goal_wp">
<goal name="WP_parameter insertion_sort.1" expl="1. loop invariant init">
......@@ -37,7 +37,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.10" expl="10. loop invariant preservation">
<proof prover="2"><result status="valid" time="1.65" steps="80"/></proof>
<proof prover="2"><result status="valid" time="1.17" steps="80"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.11" expl="11. loop variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="24"/></proof>
......@@ -59,7 +59,7 @@
</theory>
<theory name="ARM" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="InsertionSortExample" sum="035a2f3e51417e24f6e447e2c9f5b21b" expanded="true">
<theory name="InsertionSortExample" sum="8f826701fa05e53c78b726425a76d7d8" expanded="true">
<goal name="WP_parameter path_init_l2" expl="VC for path_init_l2">
<proof prover="1"><result status="valid" time="0.14"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="17"/></proof>
......
......@@ -5,12 +5,12 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="0"/>
<file name="../assigning_meanings_to_programs.mlw">
<theory name="Sum" sum="de5b5ac815e310c038a383137b72227a" expanded="true">
<theory name="Sum" sum="606dc92ebecb74d906410b581994896f" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="2"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
</theory>
<theory name="Division" sum="d23c114c7ff9509b0b89b152002ffc98" expanded="true">
<theory name="Division" sum="67dbd39ccfe310fac83f690ec134b490" expanded="true">
<goal name="WP_parameter division" expl="VC for division" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......