Commit 5f98f9b5 authored by MARCHE Claude's avatar MARCHE Claude

updated sessions

parent aa83e636
......@@ -491,332 +491,329 @@
<goal name="WP_parameter partition.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="1.92"/></proof>
<metas>
<ts_pos name="ref" arity="1" id="2327"
<ts_pos name="ref" arity="1" id="2237"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="ref"/>
</ts_pos>
<ls_pos name="zero" id="279"
<ls_pos name="zero" id="286"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="one" id="280"
<ls_pos name="one" id="287"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="one"/>
</ls_pos>
<ls_pos name="infix &lt;" id="281"
<ls_pos name="infix &lt;" id="288"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &lt;"/>
</ls_pos>
<ls_pos name="infix &gt;" id="284"
<ls_pos name="infix &gt;" id="291"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &gt;"/>
</ls_pos>
<ls_pos name="infix +" id="1450"
<ls_pos name="infix +" id="1457"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix +"/>
</ls_pos>
<ls_pos name="prefix -" id="1451"
<ls_pos name="prefix -" id="1458"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="prefix -"/>
</ls_pos>
<ls_pos name="infix *" id="1452"
<ls_pos name="infix *" id="1459"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix *"/>
</ls_pos>
<ls_pos name="prefix !" id="2333"
<ls_pos name="prefix !" id="2243"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="prefix !"/>
</ls_pos>
<ls_pos name="get" id="2479"
<ls_pos name="get" id="2389"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="2482"
<ls_pos name="set" id="2392"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="2502"
<ls_pos name="mixfix [&lt;-]" id="2412"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="const" id="2533"
<ls_pos name="const" id="2443"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="const"/>
</ls_pos>
<ls_pos name="occ" id="2918"
<ls_pos name="occ" id="2618"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ"/>
</ls_pos>
<ls_pos name="get" id="3123"
<ls_pos name="get" id="2823"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="3138"
<ls_pos name="set" id="2838"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix []" id="3163"
<ls_pos name="mixfix []" id="2863"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="mixfix []"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="3180"
<ls_pos name="mixfix [&lt;-]" id="2880"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="make" id="3281"
<ls_pos name="make" id="2981"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="make"/>
</ls_pos>
<ls_pos name="array_eq" id="3557"
<ls_pos name="array_eq" id="3257"
ip_theory="ArrayEq">
<ip_library name="array"/>
<ip_qualid name="array_eq"/>
</ls_pos>
<pr_pos name="Assoc" id="1453"
<pr_pos name="Assoc" id="1460"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Unit_def_l" id="1460"
<pr_pos name="Unit_def_l" id="1467"
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="1463"
<pr_pos name="Unit_def_r" id="1470"
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="1466"
<pr_pos name="Inv_def_l" id="1473"
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="1469"
<pr_pos name="Inv_def_r" id="1476"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_r"/>
</pr_pos>
<pr_pos name="Comm" id="1472"
<pr_pos name="Comm" id="1479"
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="1477"
<pr_pos name="Assoc" id="1484"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Assoc"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Mul_distr_l" id="1484"
<pr_pos name="Mul_distr_l" id="1491"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_l"/>
</pr_pos>
<pr_pos name="Mul_distr_r" id="1491"
<pr_pos name="Mul_distr_r" id="1498"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_r"/>
</pr_pos>
<pr_pos name="Comm" id="1509"
<pr_pos name="Comm" id="1516"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Unitary" id="1514"
<pr_pos name="Unitary" id="1521"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Unitary"/>
</pr_pos>
<pr_pos name="NonTrivialRing" id="1517"
<pr_pos name="NonTrivialRing" id="1524"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="NonTrivialRing"/>
</pr_pos>
<pr_pos name="Refl" id="1529"
<pr_pos name="Refl" id="1536"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Refl"/>
</pr_pos>
<pr_pos name="Trans" id="1532"
<pr_pos name="Trans" id="1539"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Trans"/>
</pr_pos>
<pr_pos name="Antisymm" id="1539"
<pr_pos name="Antisymm" id="1546"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Antisymm"/>
</pr_pos>
<pr_pos name="Total" id="1544"
<pr_pos name="Total" id="1551"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Total"/>
</pr_pos>
<pr_pos name="ZeroLessOne" id="1549"
<pr_pos name="ZeroLessOne" id="1556"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="ZeroLessOne"/>
</pr_pos>
<pr_pos name="CompatOrderMult" id="1557"
<pr_pos name="CompatOrderMult" id="1564"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderMult"/>
</pr_pos>
<pr_pos name="Select_eq" id="2515"
<pr_pos name="Select_eq" id="2425"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="Select_eq"/>
</pr_pos>
<pr_pos name="Select_neq" id="2524"
<pr_pos name="Select_neq" id="2434"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="Select_neq"/>
</pr_pos>
<pr_pos name="Const" id="2535"
<pr_pos name="Const" id="2445"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="Const"/>
</pr_pos>
<pr_pos name="exchange_set" id="2614"
<pr_pos name="exchange_set" id="2524"
ip_theory="MapExchange">
<ip_library name="map"/>
<ip_qualid name="exchange_set"/>
</pr_pos>
<pr_pos name="occ_right_no_add" id="2932"
<pr_pos name="occ_right_no_add" id="2632"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_right_no_add"/>
</pr_pos>
<pr_pos name="occ_bounds" id="2950"
<pr_pos name="occ_bounds" id="2650"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_bounds"/>
</pr_pos>
<pr_pos name="occ_append" id="2959"
<pr_pos name="occ_append" id="2659"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_append"/>
</pr_pos>
<pr_pos name="occ_neq" id="2970"
<pr_pos name="occ_neq" id="2670"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_neq"/>
</pr_pos>
<pr_pos name="occ_exists" id="2981"
<pr_pos name="occ_exists" id="2681"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_exists"/>
</pr_pos>
<pr_pos name="occ_pos" id="2992"
<pr_pos name="occ_pos" id="2692"
ip_theory="Occ">
<ip_library name="map"/>
<ip_qualid name="occ_pos"/>
</pr_pos>
<meta name="remove_logic">
<meta_arg_ls id="279"/>
<meta_arg_ls id="286"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="280"/>
<meta_arg_ls id="287"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="281"/>
<meta_arg_ls id="288"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="284"/>
<meta_arg_ls id="291"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1450"/>
<meta_arg_ls id="1457"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1451"/>
<meta_arg_ls id="1458"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1452"/>
<meta_arg_ls id="1459"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2333"/>
<meta_arg_ls id="2243"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2479"/>
<meta_arg_ls id="2389"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2482"/>
<meta_arg_ls id="2392"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2502"/>
<meta_arg_ls id="2412"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2533"/>
<meta_arg_ls id="2443"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="2918"/>
<meta_arg_ls id="2618"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3123"/>
<meta_arg_ls id="2823"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3138"/>
<meta_arg_ls id="2838"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3163"/>
<meta_arg_ls id="2863"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3180"/>
<meta_arg_ls id="2880"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3281"/>
<meta_arg_ls id="2981"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3557"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1453"/>
<meta_arg_ls id="3257"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1460"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1463"/>
<meta_arg_pr id="1467"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1466"/>
<meta_arg_pr id="1470"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1469"/>
<meta_arg_pr id="1473"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1472"/>
<meta_arg_pr id="1476"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1477"/>
<meta_arg_pr id="1479"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1484"/>
......@@ -825,64 +822,67 @@
<meta_arg_pr id="1491"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1509"/>
<meta_arg_pr id="1498"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1514"/>
<meta_arg_pr id="1516"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1517"/>
<meta_arg_pr id="1521"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1529"/>
<meta_arg_pr id="1524"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1532"/>
<meta_arg_pr id="1536"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1539"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1544"/>
<meta_arg_pr id="1546"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1549"/>
<meta_arg_pr id="1551"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1557"/>
<meta_arg_pr id="1556"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2515"/>
<meta_arg_pr id="1564"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2524"/>
<meta_arg_pr id="2425"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2535"/>
<meta_arg_pr id="2434"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2614"/>
<meta_arg_pr id="2445"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2524"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2932"/>
<meta_arg_pr id="2632"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2950"/>
<meta_arg_pr id="2650"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2959"/>
<meta_arg_pr id="2659"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2970"/>
<meta_arg_pr id="2670"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2981"/>
<meta_arg_pr id="2681"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2992"/>
<meta_arg_pr id="2692"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="2327"/>
<meta_arg_ts id="2237"/>
</meta>
<goal name="WP_parameter partition.4" expl="4. postcondition">
<transf name="eliminate_builtin">
......
This diff is collapsed.
This diff is collapsed.
......@@ -182,10 +182,10 @@
</goal>
<goal name="WP_parameter bellman_ford.10" expl="10. loop invariant init" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bellman_ford.10.1" expl="1." expanded="true">
<goal name="WP_parameter bellman_ford.10.1" expl="1. VC for bellman_ford" expanded="true">
<proof prover="6" timelimit="10"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.10.2" expl="2." expanded="true">
<goal name="WP_parameter bellman_ford.10.2" expl="2. VC for bellman_ford" expanded="true">
<proof prover="6" timelimit="10"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
......@@ -201,29 +201,29 @@
</goal>
<goal name="WP_parameter bellman_ford.14" expl="14. loop invariant preservation" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bellman_ford.14.1" expl="1." expanded="true">
<goal name="WP_parameter bellman_ford.14.1" expl="1. VC for bellman_ford" expanded="true">
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.14.2" expl="2." expanded="true">
<goal name="WP_parameter bellman_ford.14.2" expl="2. VC for bellman_ford" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="WP_parameter bellman_ford.14.2.1" expl="1." expanded="true">
<goal name="WP_parameter bellman_ford.14.2.1" expl="1. VC for bellman_ford" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bellman_ford.14.2.1.1" expl="1." expanded="true">
<goal name="WP_parameter bellman_ford.14.2.1.1" expl="1. VC for bellman_ford" expanded="true">
<proof prover="2" timelimit="30"><result status="valid" time="0.35"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.14.2.1.2" expl="2." expanded="true">
<goal name="WP_parameter bellman_ford.14.2.1.2" expl="2. VC for bellman_ford" expanded="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.68"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="1.50"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.14.2.1.3" expl="3." expanded="true">
<goal name="WP_parameter bellman_ford.14.2.1.3" expl="3. VC for bellman_ford" expanded="true">
<proof prover="2"><result status="valid" time="18.39"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.14.2.1.4" expl="4." expanded="true">
<goal name="WP_parameter bellman_ford.14.2.1.4" expl="4. VC for bellman_ford" expanded="true">
<proof prover="2" timelimit="33"><result status="valid" time="0.13"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.14.2.1.5" expl="5." expanded="true">
<goal name="WP_parameter bellman_ford.14.2.1.5" expl="5. VC for bellman_ford" expanded="true">
<proof prover="2"><result status="valid" time="12.74"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="0.41"/></proof>
</goal>
......@@ -282,10 +282,10 @@
</goal>
<goal name="WP_parameter bellman_ford.22" expl="22. loop invariant preservation" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bellman_ford.22.1" expl="1." expanded="true">
<goal name="WP_parameter bellman_ford.22.1" expl="1. VC for bellman_ford" expanded="true">
<proof prover="6" timelimit="15" memlimit="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.22.2" expl="2." expanded="true">
<goal name="WP_parameter bellman_ford.22.2" expl="2. VC for bellman_ford" expanded="true">
<proof prover="6" timelimit="31" memlimit="0"><result status="valid" time="0.27"/></proof>
</goal>
</transf>
......