Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 29df0abf authored by MARCHE Claude's avatar MARCHE Claude

Proofs of VCs of test functions

parent 2e98995c
......@@ -1019,6 +1019,26 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter run"
locfile="../euler001.mlw"
loclnum="171" loccnumb="6" loccnume="9"
expl="VC for run"
sum="91534c2448d932ea00c55048312c72ef"
proved="true"
expanded="true"
shape="ainfix &gt;=c1000c1">
<label
name="expl:VC for run"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -1057,6 +1057,26 @@
</goal>
</transf>
</goal>
<goal
name="WP_parameter run"
locfile="../euler002.mlw"
loclnum="153" loccnumb="6" loccnume="9"
expl="VC for run"
sum="04e345d476f42eaab8e032987d2d4911"
proved="true"
expanded="true"
shape="ainfix &gt;=c4000000c0">
<label
name="expl:VC for run"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -8,7 +8,7 @@
<file
name="../fact.mlw"
verified="true"
expanded="false">
expanded="true">
<theory
name="FactRecursive"
locfile="../fact.mlw"
......@@ -35,17 +35,97 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test0"
locfile="../fact.mlw"
loclnum="12" loccnumb="6" loccnume="11"
expl="VC for test0"
sum="aea028b876acf4946b6db9a63fd7a7a3"
proved="true"
expanded="false"
shape="ainfix &gt;=c0c0">
<label
name="expl:VC for test0"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test1"
locfile="../fact.mlw"
loclnum="13" loccnumb="6" loccnume="11"
expl="VC for test1"
sum="910fe73776598665c2dd70b53c2e9d65"
proved="true"
expanded="false"
shape="ainfix &gt;=c1c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test7"
locfile="../fact.mlw"
loclnum="14" loccnumb="6" loccnume="11"
expl="VC for test7"
sum="9ca8630b4e0b458b8630d2857d269ca2"
proved="true"
expanded="false"
shape="ainfix &gt;=c7c0">
<label
name="expl:VC for test7"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test42"
locfile="../fact.mlw"
loclnum="15" loccnumb="6" loccnume="12"
expl="VC for test42"
sum="75bcbb12e431f4f88f182bfe38e6860c"
proved="true"
expanded="false"
shape="ainfix &gt;=c42c0">
<label
name="expl:VC for test42"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
<theory
name="FactImperative"
locfile="../fact.mlw"
loclnum="14" loccnumb="7" loccnume="21"
loclnum="19" loccnumb="7" loccnume="21"
verified="true"
expanded="true">
<goal
name="WP_parameter fact_imp"
locfile="../fact.mlw"
loclnum="19" loccnumb="6" loccnume="14"
loclnum="24" loccnumb="6" loccnume="14"
expl="VC for fact_imp"
sum="22dba464004dc13cd33fb20c7026c902"
proved="true"
......@@ -62,6 +142,86 @@
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter test0"
locfile="../fact.mlw"
loclnum="36" loccnumb="6" loccnume="11"
expl="VC for test0"
sum="a8b9cd2df638dd3589749e8b1c1925c8"
proved="true"
expanded="false"
shape="ainfix &gt;=c0c0">
<label
name="expl:VC for test0"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test1"
locfile="../fact.mlw"
loclnum="37" loccnumb="6" loccnume="11"
expl="VC for test1"
sum="6fe053dfa12467d16e351946433a60e9"
proved="true"
expanded="false"
shape="ainfix &gt;=c1c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test7"
locfile="../fact.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="VC for test7"
sum="5ae57b9a90987a77a43dd63de5668a71"
proved="true"
expanded="false"
shape="ainfix &gt;=c7c0">
<label
name="expl:VC for test7"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test42"
locfile="../fact.mlw"
loclnum="39" loccnumb="6" loccnume="12"
expl="VC for test42"
sum="8eb550321610bbff0d76cdbc4bba9167"
proved="true"
expanded="false"
shape="ainfix &gt;=c42c0">
<label
name="expl:VC for test42"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -177,6 +177,8 @@
loclnum="46" loccnumb="7" loccnume="18"
verified="true"
expanded="true">
<label
name="recursive version, using ghost code"/>
<goal
name="WP_parameter fib_aux"
locfile="../fibonacci.mlw"
......@@ -256,6 +258,8 @@
loclnum="63" loccnumb="7" loccnume="20"
verified="true"
expanded="true">
<label
name="recursive version, without ghost code"/>
<goal
name="WP_parameter fib_aux"
locfile="../fibonacci.mlw"
......@@ -496,6 +500,86 @@
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter test0"
locfile="../fibonacci.mlw"
loclnum="148" loccnumb="6" loccnume="11"
expl="VC for test0"
sum="c2da3f9d6f2879772573b45e78df0b25"
proved="true"
expanded="true"
shape="ainfix &gt;=c0c0">
<label
name="expl:VC for test0"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test1"
locfile="../fibonacci.mlw"
loclnum="149" loccnumb="6" loccnume="11"
expl="VC for test1"
sum="4b533d90b4f15f8b797dbc8904533deb"
proved="true"
expanded="true"
shape="ainfix &gt;=c1c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter test7"
locfile="../fibonacci.mlw"
loclnum="150" loccnumb="6" loccnume="11"
expl="VC for test7"
sum="61ab7e4eb16c413ec804eb22e8eae409"
proved="true"
expanded="true"
shape="ainfix &gt;=c7c0">
<label
name="expl:VC for test7"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test42"
locfile="../fibonacci.mlw"
loclnum="151" loccnumb="6" loccnume="12"
expl="VC for test42"
sum="6cd458a64cacb588a18255486b6946d5"
proved="true"
expanded="true"
shape="ainfix &gt;=c42c0">
<label
name="expl:VC for test42"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -26,14 +26,14 @@
expl="VC for enum"
sum="1a8be7972b22f1230da0b2838f3e739c"
proved="true"
expanded="true"
expanded="false"
shape="Cainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aEmptyainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FACfaEmptyainfix =V7V2Oainfix =V6V2aNodeVwVV0aNodeVVVV0F">
<label
name="expl:VC for enum"/>
<transf
name="split_goal"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter enum.1"
locfile="../same_fringe.mlw"
......@@ -41,7 +41,7 @@
expl="1. postcondition"
sum="beb2f0007d1c94eff394e1c707fe0604"
proved="true"
expanded="true"
expanded="false"
shape="postconditionCainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aEmptytaNodeVVVV0F">
<label
name="expl:VC for enum"/>
......@@ -61,7 +61,7 @@
expl="2. variant decrease"
sum="02b6e4c6c7ee0c7cd5d7e4f8f06d0229"
proved="true"
expanded="true"
expanded="false"
shape="variant decreaseCtaEmptyCfaEmptyainfix =V6V2Oainfix =V5V2aNodeVwVV0aNodeVVVV0F">
<label
name="expl:VC for enum"/>
......@@ -81,7 +81,7 @@
expl="3. postcondition"
sum="1b239bd1fbbbf378fce0d04f1b444a27"
proved="true"
expanded="true"
expanded="false"
shape="postconditionCtaEmptyainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FaNodeVVVV0F">
<label
name="expl:VC for enum"/>
......@@ -103,14 +103,14 @@
expl="VC for eq_enum"
sum="ec562dea41cb51c7a73addc6ea779761"
proved="true"
expanded="true"
expanded="false"
shape="CCiNainfix =aenum_elementsV0aenum_elementsV1ainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFAainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4Fainfix =V5V2aNextVVVNainfix =aenum_elementsV0aenum_elementsV1wV0aNextVVVCainfix =aenum_elementsV0aenum_elementsV1aDoneNainfix =aenum_elementsV0aenum_elementsV1wV0aDoneV1F">
<label
name="expl:VC for eq_enum"/>
<transf
name="split_goal"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter eq_enum.1"
locfile="../same_fringe.mlw"
......@@ -118,7 +118,7 @@
expl="1. variant decrease"
sum="6e39f74ab276bf4e82c48ce96319d1c3"
proved="true"
expanded="true"
expanded="false"
shape="variant decreaseCCainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FIainfix =V5V2aNextVVVtwV0aNextVVVtaDoneV1F">
<label
name="expl:VC for eq_enum"/>
......@@ -146,7 +146,7 @@
expl="2. postcondition"
sum="0ca3e70f3dd4a563e25dfe755e04e7f6"
proved="true"
expanded="true"
expanded="false"
shape="postconditionCCainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFIainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FIainfix =V5V2aNextVVVtwV0aNextVVVtaDoneV1F">
<label
name="expl:VC for eq_enum"/>
......@@ -186,7 +186,7 @@
expl="4. postcondition"
sum="f928c51aa703ee5accb2189f529d32d2"
proved="true"
expanded="true"
expanded="false"
shape="postconditionCCtaNextVVVNainfix =aenum_elementsV0aenum_elementsV1wV0aNextVVVtaDoneV1F">
<label
name="expl:VC for eq_enum"/>
......@@ -206,7 +206,7 @@
expl="5. postcondition"
sum="9625235d246c1c6acb7ee6635ea3f868"
proved="true"
expanded="true"
expanded="false"
shape="postconditionCtaNextVVVCainfix =aenum_elementsV0aenum_elementsV1aDonetwV0aDoneV1F">
<label
name="expl:VC for eq_enum"/>
......@@ -226,7 +226,7 @@
expl="6. postcondition"
sum="63d7a3c44e709bf4fa95f03d644d80aa"
proved="true"
expanded="true"
expanded="false"
shape="postconditionCtaNextVVVCtaDoneNainfix =aenum_elementsV0aenum_elementsV1wV0aDoneV1F">
<label
name="expl:VC for eq_enum"/>
......@@ -248,7 +248,7 @@
expl="VC for same_fringe"
sum="5bc6c55be26f125ba6bf2acefd6c510e"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =aelementsV0aelementsV1qainfix =V4aTrueIainfix =aenum_elementsV3aenum_elementsV2qainfix =V4aTrueFIainfix =aenum_elementsV3ainfix ++aelementsV0aenum_elementsaDoneFIainfix =aenum_elementsV2ainfix ++aelementsV1aenum_elementsaDoneFF">
<label
name="expl:VC for same_fringe"/>
......@@ -261,6 +261,253 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test1"
locfile="../same_fringe.mlw"
loclnum="63" loccnumb="6" loccnume="11"
expl="VC for test1"
sum="287fbb8541919b10fb1c5b3caf528ea9"
proved="true"
expanded="false"
shape="t">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test2"
locfile="../same_fringe.mlw"
loclnum="64" loccnumb="6" loccnume="11"
expl="VC for test2"
sum="287fbb8541919b10fb1c5b3caf528ea9"
proved="true"
expanded="false"
shape="t">
<label
name="expl:VC for test2"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test3"
locfile="../same_fringe.mlw"
loclnum="65" loccnumb="6" loccnume="11"
expl="VC for test3"
sum="287fbb8541919b10fb1c5b3caf528ea9"
proved="true"
expanded="false"
shape="t">
<label
name="expl:VC for test3"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter leaf"
locfile="../same_fringe.mlw"
loclnum="70" loccnumb="6" loccnume="10"
expl="VC for leaf"
sum="3400f23f9ad433031bf43c27ae1ed177"
proved="true"
expanded="false"
shape="t">
<label
name="expl:VC for leaf"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test4"
locfile="../same_fringe.mlw"
loclnum="72" loccnumb="6" loccnume="11"
expl="VC for test4"
sum="3400f23f9ad433031bf43c27ae1ed177"
proved="true"
expanded="false"
shape="t">
<label
name="expl:VC for test4"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test5"
locfile="../same_fringe.mlw"
loclnum="73" loccnumb="6" loccnume="11"
expl="VC for test5"
sum="3400f23f9ad433031bf43c27ae1ed177"
proved="true"
expanded="false"
shape="t">
<label
name="expl:VC for test5"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
<theory
name="Test"
locfile="../same_fringe.mlw"
loclnum="77" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="WP_parameter test1"
locfile="../same_fringe.mlw"
loclnum="82" loccnumb="6" loccnume="11"
expl="VC for test1"
sum="245f6c881b394e2917602c2cbeee7937"
proved="true"
expanded="false"
shape="t">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test2"
locfile="../same_fringe.mlw"
loclnum="83" loccnumb="6" loccnume="11"
expl="VC for test2"
sum="245f6c881b394e2917602c2cbeee7937"
proved="true"
expanded="false"
shape="t">
<label
name="expl:VC for test2"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>