Commit 74e13e2e authored by MARCHE Claude's avatar MARCHE Claude

updated sessions

parent 323ddc94
This source diff could not be displayed because it is too large. You can view the blob instead.
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd"> <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.1"/> <prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.2"/> <prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5"
<prover id="2" name="CVC3" version="2.4.1"/> memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl2"/> <prover id="2" name="Z3" version="2.19" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="2.19"/> <prover id="3" name="Coq" version="8.4pl3" timelimit="30" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2"/> <prover id="4" name="CVC3" version="2.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<file name="../double.why" verified="true" <file name="../double.why" verified="true"
expanded="true"> expanded="true">
<theory name="BV_double" locfile="../double.why" <theory name="BV_double" verified="true">
loclnum="1" loccnumb="7" loccnume="16" verified="true">
</theory> </theory>
<theory name="TestDouble" locfile="../double.why" <theory name="TestDouble" verified="true"
loclnum="65" loccnumb="7" loccnume="17" verified="true"
expanded="true"> expanded="true">
<goal name="nth_one1" locfile="../double.why" <goal name="nth_one1" sum="9426856b7db1eaa0a7fbf98d0a1d6511" proved="true"
loclnum="73" loccnumb="8" loccnume="16" expanded="true"
sum="9426856b7db1eaa0a7fbf98d0a1d6511" proved="true" expanded="true"
shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c51Aainfix &lt;=c0V0F"> shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c51Aainfix &lt;=c0V0F">
<proof prover="0" timelimit="3" <proof prover="1" timelimit="3">
memlimit="1000">
<result status="valid" time="0.33"/> <result status="valid" time="0.33"/>
</proof> </proof>
</goal> </goal>
<goal name="nth_one2" locfile="../double.why" <goal name="nth_one2" sum="b1c633079fda4d75118758023d1bd9d6" proved="true"
loclnum="74" loccnumb="8" loccnume="16" expanded="true"
sum="b1c633079fda4d75118758023d1bd9d6" proved="true" expanded="true"
shape="ainfix =anthaoneV0aTrueIainfix &lt;=V0c61Aainfix &lt;=c52V0F"> shape="ainfix =anthaoneV0aTrueIainfix &lt;=V0c61Aainfix &lt;=c52V0F">
<proof prover="0" timelimit="3" <proof prover="1" timelimit="3">
memlimit="1000">
<result status="valid" time="0.23"/> <result status="valid" time="0.23"/>
</proof> </proof>
</goal> </goal>
<goal name="nth_one3" locfile="../double.why" <goal name="nth_one3" sum="7b13e3cc4204cfbf0bcadc9604a16925" proved="true"
loclnum="75" loccnumb="8" loccnume="16"
sum="7b13e3cc4204cfbf0bcadc9604a16925" proved="true"
shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c63Aainfix &lt;=c62V0F"> shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c63Aainfix &lt;=c62V0F">
<proof prover="0" timelimit="5" <proof prover="1">
memlimit="1000">
<result status="valid" time="0.31"/> <result status="valid" time="0.31"/>
</proof> </proof>
</goal> </goal>
<goal name="sign_one" locfile="../double.why" <goal name="sign_one" sum="bdda75f77974f193214e8a50e2cd6d59" proved="true"
loclnum="77" loccnumb="8" loccnume="16"
sum="bdda75f77974f193214e8a50e2cd6d59" proved="true"
shape="ainfix =asignaoneaFalse"> shape="ainfix =asignaoneaFalse">
<proof prover="0" timelimit="5" <proof prover="0">
memlimit="1000">
<result status="valid" time="0.03"/> <result status="valid" time="0.03"/>
</proof> </proof>
<proof prover="1" timelimit="5" <proof prover="1">
memlimit="1000">
<result status="valid" time="0.02"/>
</proof>
<proof prover="2" timelimit="5"
memlimit="1000">
<result status="valid" time="0.03"/> <result status="valid" time="0.03"/>
</proof> </proof>
<proof prover="4" timelimit="5" <proof prover="2">
memlimit="1000">
<result status="valid" time="0.11"/> <result status="valid" time="0.11"/>
</proof> </proof>
<proof prover="5" timelimit="5" <proof prover="4">
memlimit="1000"> <result status="valid" time="0.02"/>
</proof>
<proof prover="5">
<result status="valid" time="0.11"/> <result status="valid" time="0.11"/>
</proof> </proof>
</goal> </goal>
<goal name="exp_one" locfile="../double.why" <goal name="exp_one" sum="0c3504d58a9734848a0cbc03bc51d27d" proved="true"
loclnum="78" loccnumb="8" loccnume="15"
sum="0c3504d58a9734848a0cbc03bc51d27d" proved="true"
shape="ainfix =aexpaonec1023"> shape="ainfix =aexpaonec1023">
<proof prover="0" timelimit="30" <proof prover="1" timelimit="30">
memlimit="1000">
<result status="valid" time="1.63"/> <result status="valid" time="1.63"/>
</proof> </proof>
<proof prover="3" timelimit="30" memlimit="1000" <proof prover="3" edited="double_TestDouble_exp_one_1.v">
edited="double_TestDouble_exp_one_1.v">
<result status="valid" time="1.21"/> <result status="valid" time="1.21"/>
</proof> </proof>
</goal> </goal>
<goal name="mantissa_one" locfile="../double.why" <goal name="mantissa_one" sum="e7fa2f72bb2aada4371ebb33b3cc263e"
loclnum="79" loccnumb="8" loccnume="20" proved="true"
sum="e7fa2f72bb2aada4371ebb33b3cc263e" proved="true"
shape="ainfix =amantissaaonec0"> shape="ainfix =amantissaaonec0">
<proof prover="0" timelimit="5" <proof prover="1">
memlimit="1000">
<result status="valid" time="0.09"/> <result status="valid" time="0.09"/>
</proof> </proof>
<proof prover="4" timelimit="5" <proof prover="2">
memlimit="1000">
<result status="valid" time="0.69"/> <result status="valid" time="0.69"/>
</proof> </proof>
<proof prover="5" timelimit="11" <proof prover="5" timelimit="11">
memlimit="1000">
<result status="valid" time="3.36"/> <result status="valid" time="3.36"/>
</proof> </proof>
</goal> </goal>
<goal name="double_value_of_1" locfile="../double.why" <goal name="double_value_of_1" sum="a43ae53878e69bc2d59a96e436eb69b9"
loclnum="81" loccnumb="8" loccnume="25" proved="true"
sum="a43ae53878e69bc2d59a96e436eb69b9" proved="true"
shape="ainfix =adouble_of_bv64aonec1.0"> shape="ainfix =adouble_of_bv64aonec1.0">
<proof prover="0" timelimit="5" <proof prover="0">
memlimit="1000">
<result status="valid" time="0.04"/>
</proof>
<proof prover="1" timelimit="5"
memlimit="1000">
<result status="valid" time="0.03"/> <result status="valid" time="0.03"/>
</proof> </proof>
<proof prover="2" timelimit="5" <proof prover="1">
memlimit="1000"> <result status="valid" time="0.04"/>
</proof>
<proof prover="4">
<result status="valid" time="0.03"/> <result status="valid" time="0.03"/>
</proof> </proof>
</goal> </goal>
......
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd"> <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.1"/> <prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.2"/> <prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5"
<prover id="2" name="CVC3" version="2.4.1"/> memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl2"/> <prover id="2" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="4" name="Z3" version="2.19"/> <prover id="3" name="Coq" version="8.4pl3" timelimit="5" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="30"
memlimit="1000"/>
<file name="../bresenham.mlw" verified="true" <file name="../bresenham.mlw" verified="true"
expanded="true"> expanded="true">
<theory name="M" locfile="../bresenham.mlw" <theory name="M" verified="true"
loclnum="3" loccnumb="7" loccnume="8" verified="true"
expanded="true"> expanded="true">
<goal name="closest" locfile="../bresenham.mlw" <goal name="closest" sum="472a5d038bef87fcbfb94fa2e7253191" proved="true"
loclnum="34" loccnumb="8" loccnume="15" expanded="true"
sum="472a5d038bef87fcbfb94fa2e7253191" proved="true" expanded="true"
shape="ainfix &lt;=aabsainfix -ainfix *V0V1V2aabsainfix -ainfix *V0V3V2FIainfix &lt;=aabsainfix -ainfix *ainfix *c2V0V1ainfix *c2V2V0F"> shape="ainfix &lt;=aabsainfix -ainfix *V0V1V2aabsainfix -ainfix *V0V3V2FIainfix &lt;=aabsainfix -ainfix *ainfix *c2V0V1ainfix *c2V2V0F">
<proof prover="3" timelimit="5" memlimit="1000" <proof prover="3" edited="bresenham_M_closest_1.v">
edited="bresenham_M_closest_1.v">
<result status="valid" time="1.29"/> <result status="valid" time="1.29"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham" locfile="../bresenham.mlw" <goal name="WP_parameter bresenham" expl="VC for bresenham"
loclnum="39" loccnumb="6" loccnume="15" expl="VC for bresenham"
sum="c273b5a8d99bf83f043f35169bda938e" proved="true" expanded="true" sum="c273b5a8d99bf83f043f35169bda938e" proved="true" expanded="true"
shape="iainfix &lt;=V5ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V5Aainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1Fainfix &lt;=V6ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V6Aainfix =V6ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V6ainfix +V1ainfix *c2ay2Fainfix &lt;V1c0AabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFAainfix &lt;=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Aainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix &lt;=c0V0Lax2"> shape="iainfix &lt;=V5ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V5Aainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1Fainfix &lt;=V6ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V6Aainfix =V6ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V6ainfix +V1ainfix *c2ay2Fainfix &lt;V1c0AabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFAainfix &lt;=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Aainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix &lt;=c0V0Lax2">
<label name="expl:VC for bresenham"/> <label name="expl:VC for bresenham"/>
<transf name="split_goal" proved="true" <transf name="split_goal" proved="true"
expanded="true"> expanded="true">
<goal name="WP_parameter bresenham.1" locfile="../bresenham.mlw" <goal name="WP_parameter bresenham.1" expl="1. loop invariant init"
loclnum="39" loccnumb="6" loccnume="15" expl="1. loop invariant init"
sum="ed65b836fad1f9e81238b52f26b3793b" proved="true" expanded="true" sum="ed65b836fad1f9e81238b52f26b3793b" proved="true" expanded="true"
shape="loop invariant initainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix &lt;=c0V0Lax2"> shape="loop invariant initainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix &lt;=c0V0Lax2">
<label name="expl:VC for bresenham"/> <label name="expl:VC for bresenham"/>
<proof prover="0" timelimit="5" <proof prover="0">
memlimit="1000">
<result status="valid" time="0.01"/>
</proof>
<proof prover="2" timelimit="10"
memlimit="0">
<result status="valid" time="0.00"/> <result status="valid" time="0.00"/>
</proof> </proof>
<proof prover="4" timelimit="10" <proof prover="1">
memlimit="0"> <result status="valid" time="0.01"/>
</proof>
<proof prover="2">
<result status="valid" time="0.02"/> <result status="valid" time="0.02"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.2" locfile="../bresenham.mlw" <goal name="WP_parameter bresenham.2" expl="2. loop invariant init"
loclnum="39" loccnumb="6" loccnume="15" expl="2. loop invariant init"
sum="1f431337ccd802b522a98f30abadccae" proved="true" expanded="true" sum="1f431337ccd802b522a98f30abadccae" proved="true" expanded="true"
shape="loop invariant initainfix &lt;=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Iainfix &lt;=c0V0Lax2"> shape="loop invariant initainfix &lt;=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Iainfix &lt;=c0V0Lax2">
<label name="expl:VC for bresenham"/> <label name="expl:VC for bresenham"/>
<proof prover="0" timelimit="5" <proof prover="1">
memlimit="1000">
<result status="valid" time="0.01"/> <result status="valid" time="0.01"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.3" locfile="../bresenham.mlw" <goal name="WP_parameter bresenham.3" expl="3. assertion"
loclnum="39" loccnumb="6" loccnume="15" expl="3. assertion"
sum="34351a2fcaf0596c940f5c34b7545156" proved="true" expanded="true" sum="34351a2fcaf0596c940f5c34b7545156" proved="true" expanded="true"
shape="assertionabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2"> shape="assertionabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
<label name="expl:VC for bresenham"/> <label name="expl:VC for bresenham"/>
<proof prover="0" timelimit="30" <proof prover="1" timelimit="30">
memlimit="1000">
<result status="valid" time="1.86"/> <result status="valid" time="1.86"/>
</proof> </proof>
<proof prover="1" timelimit="30" <proof prover="4">
memlimit="1000">
<result status="valid" time="1.80"/> <result status="valid" time="1.80"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.4" locfile="../bresenham.mlw" <goal name="WP_parameter bresenham.4"
loclnum="39" loccnumb="6" loccnume="15"
expl="4. loop invariant preservation" expl="4. loop invariant preservation"
sum="74d2dd38d47dd2952bd12873b5e1bd85" proved="true" expanded="true" sum="74d2dd38d47dd2952bd12873b5e1bd85" proved="true" expanded="true"
shape="loop invariant preservationainfix =V4ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2"> shape="loop invariant preservationainfix =V4ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
<label name="expl:VC for bresenham"/> <label name="expl:VC for bresenham"/>
<proof prover="0" timelimit="5" <proof prover="0">
memlimit="1000">
<result status="valid" time="0.02"/> <result status="valid" time="0.02"/>
</proof> </proof>
<proof prover="2" timelimit="10" <proof prover="1">
memlimit="0">
<result status="valid" time="0.02"/> <result status="valid" time="0.02"/>
</proof> </proof>
<proof prover="4" timelimit="10" <proof prover="2">
memlimit="0">
<result status="valid" time="0.01"/> <result status="valid" time="0.01"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.5" locfile="../bresenham.mlw" <goal name="WP_parameter bresenham.5"
loclnum="39" loccnumb="6" loccnume="15"
expl="5. loop invariant preservation" expl="5. loop invariant preservation"
sum="49fe8a7e169678e5aaf592b78ff8cebd" proved="true" expanded="true" sum="49fe8a7e169678e5aaf592b78ff8cebd" proved="true" expanded="true"
shape="loop invariant preservationainfix &lt;=V4ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V4Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2"> shape="loop invariant preservationainfix &lt;=V4ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V4Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
<label name="expl:VC for bresenham"/> <label name="expl:VC for bresenham"/>
<proof prover="0" timelimit="5" <proof prover="1">
memlimit="1000">
<result status="valid" time="0.02"/> <result status="valid" time="0.02"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.6" locfile="../bresenham.mlw" <goal name="WP_parameter bresenham.6"
loclnum="39" loccnumb="6" loccnume="15"
expl="6. loop invariant preservation" expl="6. loop invariant preservation"
sum="3ac02f3d978219fa286a8d3d74638379" proved="true" expanded="true" sum="3ac02f3d978219fa286a8d3d74638379" proved="true" expanded="true"
shape="loop invariant preservationainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2"> shape="loop invariant preservationainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
<label name="expl:VC for bresenham"/> <label name="expl:VC for bresenham"/>
<proof prover="2" timelimit="10" <proof prover="0">
memlimit="0">
<result status="valid" time="0.02"/> <result status="valid" time="0.02"/>
</proof> </proof>
<proof prover="4" timelimit="10" <proof prover="2">
memlimit="0">
<result status="valid" time="0.28"/> <result status="valid" time="0.28"/>
</proof> </proof>
</goal> </goal>
<goal name="WP_parameter bresenham.7" locfile="../bresenham.mlw" <goal name="WP_parameter bresenham.7"
loclnum="39" loccnumb="6" loccnume="15"
expl="7. loop invariant preservation" expl="7. loop invariant preservation"
sum="ff4fa86e8ee958cfa266e050e0feb12a" proved="true" expanded="true" sum="ff4fa86e8ee958cfa266e050e0feb12a" proved="true" expanded="true"
shape="loop invariant preservationainfix &lt;=V5ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V5Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2"> shape="loop invariant preservationainfix &lt;=V5ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V5Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix &lt;V1c0IabestV3V2Iainfix &lt;=V1ainfix *c2ay2Aainfix &lt;=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix &lt;=V3V0Aainfix &lt;=c0V3FFIainfix &lt;=c0V0Lax2">
<label name="expl:VC for bresenham"/> <label name="expl:VC for bresenham"/>
<proof prover="0" timelimit="5" <proof prover="1">
memlimit="1000">
<result status="valid" time="0.02"/> <result status="valid" time="0.02"/>
</proof> </proof>
</goal> </goal>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd"> <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl2"/> <prover id="0" name="Coq" version="8.4pl3" timelimit="10" memlimit="0"/>
<file name="../12934.why" verified="true" <file name="../12934.why" verified="true"
expanded="true"> expanded="true">
<theory name="BTS12934" locfile="../12934.why" <theory name="BTS12934" verified="true"
loclnum="2" loccnumb="7" loccnume="15" verified="true"
expanded="true"> expanded="true">
<goal name="t" locfile="../12934.why" <goal name="t" sum="aca30d067ede9d92da38517bfeb6e6e6" proved="true"
loclnum="8" loccnumb="7" loccnume="8" expanded="true"
sum="aca30d067ede9d92da38517bfeb6e6e6" proved="true" expanded="true"
shape="t"> shape="t">
<proof prover="0" timelimit="10" memlimit="0" <proof prover="0" edited="12934_BTS12934_t_1.v">
edited="12934_BTS12934_t_1.v">
<result status="valid" time="1.01"/> <result status="valid" time="1.01"/>
</proof> </proof>
</goal> </goal>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd"> <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl2"/> <prover id="0" name="Coq" version="8.4pl3" timelimit="10" memlimit="0"/>
<file name="../13849.why" <file name="../13849.why"
verified="true"> verified="true">
<theory name="T" locfile="../13849.why" <theory name="T" verified="true"
loclnum="4" loccnumb="7" loccnume="8" verified="true"
expanded="true"> expanded="true">
<goal name="x" locfile="../13849.why" <goal name="x" sum="d3791e53f665e657d24f40c36be3a764" proved="true"
loclnum="19" loccnumb="6" loccnume="7" expanded="true"
sum="d3791e53f665e657d24f40c36be3a764" proved="true" expanded="true"
shape="ainfix =ab1ab2"> shape="ainfix =ab1ab2">
<proof prover="0" timelimit="10" memlimit="0" <proof prover="0" edited="13849_T_x_2.v">
edited="13849_T_x_2.v">
<result status="valid" time="0.99"/> <result status="valid" time="0.99"/>
</proof> </proof>
</goal> </goal>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd"> <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl2"/> <prover id="0" name="Coq" version="8.4pl3" timelimit="5" memlimit="0"/>
<file name="../13854.why" <file name="../13854.why"
verified="true"> verified="true">
<theory name="T" locfile="../13854.why" <theory name="T" verified="true"
loclnum="1" loccnumb="7" loccnume="8" verified="true"
expanded="true"> expanded="true">
<goal name="g" locfile="../13854.why" <goal name="g" sum="a3d33ce2b1b1019d546ea64443df10d7" proved="true"
loclnum="6" loccnumb="7" loccnume="8" expanded="true"
sum="a3d33ce2b1b1019d546ea64443df10d7" proved="true" expanded="true"
shape="ainfix =aTuple0afaTuple0"> shape="ainfix =aTuple0afaTuple0">
<proof prover="0" timelimit="5" memlimit="0" <proof prover="0" edited="13854_T_g_1.v">
edited="13854_T_g_1.v">
<result status="valid" time="0.95"/> <result status="valid" time="0.95"/>
</proof> </proof>
</goal> </goal>
<goal name="x" locfile="../13854.why" <goal name="x" sum="6cd7d913500bef42fd9c6bf396e93e2d" proved="true"
loclnum="8" loccnumb="7" loccnume="8" expanded="true"
sum="6cd7d913500bef42fd9c6bf396e93e2d" proved="true" expanded="true"
shape="Nainfix =aAaTuple0aB"> shape="Nainfix =aAaTuple0aB">
<proof prover="0" timelimit="5" memlimit="0" <proof prover="0" edited="13854_T_x_1.v">
edited="13854_T_x_1.v">
<result status="valid" time="0.96"/> <result status="valid" time="0.96"/>
</proof> </proof>
</goal> </goal>
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd"> <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.1"/> <prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl2"/> <prover id="1" name="Coq" version="8.4pl3" timelimit="5" memlimit="0"/>
<file name="../tree_max.mlw" verified="true" <file name="../tree_max.mlw" verified="true"
expanded="true"> expanded="true">
<theory name="BinTree" locfile="../tree_max.mlw" <theory name="BinTree" verified="true"
loclnum="26" loccnumb="7" loccnume="14" verified="true"
expanded="true"> expanded="true">
<goal name="ge_trans" locfile="../tree_max.mlw" <goal name="ge_trans" sum="47019ef989e9cebbabc98d94bed53cd9" proved="true"
loclnum="47" loccnumb="8" loccnume="16" expanded="true"
sum="47019ef989e9cebbabc98d94bed53cd9" proved="true" expanded="true"
shape="age_treeV1V0Iage_treeV2V0Aainfix &gt;=V1V2F"> shape="age_treeV1V0Iage_treeV2V0Aainfix &gt;=V1V2F">
<proof prover="1" timelimit="5" memlimit="0" <proof prover="1" edited="tree_max_BinTree_ge_trans_1.v">
edited="tree_max_BinTree_ge_trans_1.v">
<result status="valid" time="0.99"/> <result status="valid" time="0.99"/>
</proof> </proof>
</goal> </goal>
</theory> </theory>
<theory name="TreeMax" locfile="../tree_max.mlw" <theory name="TreeMax" verified="true"
loclnum="52" loccnumb="7" loccnume="14" verified="true"
expanded="true"> expanded="true">
<goal name="WP_parameter max_aux" locfile="../tree_max.mlw" <goal name="WP_parameter max_aux" expl="VC for max_aux"
loclnum="58" loccnumb="10" loccnume="17" expl="VC for max_aux"
sum="8511822819fb1b5df06e65fdb18f5f10" proved="true" expanded="true" sum="8511822819fb1b5df06e65fdb18f5f10" proved="true" expanded="true"
shape="Cainfix &gt;=V1V1Aage_treeV1V0aNullamemV7V0Oainfix =V7V1Aainfix &gt;=V7V1Aage_treeV7V0IamemV7V3Oainfix =V7V6Aainfix &gt;=V7V6Aage_treeV7V3FACfaNullainfix =V9V3Oainfix =V8V3aTreewVVV0IamemV6V4Oainfix =V6V5Aainfix &gt;=V6V5Aage_treeV6V4FACfaNullainfix =V11V4Oainfix =V10V4aTreewVVV0LamaxV2V1aTreeVVVV0F"> shape="Cainfix &gt;=V1V1Aage_treeV1V0aNullamemV7V0Oainfix =V7V1Aainfix &gt;=V7V1Aage_treeV7V0IamemV7V3Oainfix =V7V6Aainfix &gt;=V7V6Aage_treeV7V3FACfaNullainfix =V9V3Oainfix =V8V3aTreewVVV0IamemV6V4Oainfix =V6V5Aainfix &gt;=V6V5Aage_treeV6V4FACfaNullainfix =V11V4Oainfix =V10V4aTreewVVV0LamaxV2V1aTreeVVVV0F">
<label name="expl:VC for max_aux"/> <label name="expl:VC for max_aux"/>
<proof prover="0" timelimit="5" <proof prover="0">
memlimit="0">
<result status="valid" time="0.04"/>