Skip to content

GitLab

why3
why3
Commit e4267f5c authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Task checksum does not depend on Pretty anymore

parent f0217599
Hide whitespace changes
Inline Side-by-side
Showing with 1659 additions and 1651 deletions
examples/bts/12475/why3session.xml
View file @ e4267f5c
......@@ -2,28 +2,25 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="bts/12475/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../12475.why" verified="true" expanded="true">
<theory name="Stmt" verified="true" expanded="true">
<goal name="toto" sum="fb9c382631eb3331b29b3e2e91edb9ef" proved="true" expanded="true" shape="ainfix <V0ainfix +aroundaUpV0c1.F">
<goal name="toto" sum="70b485a4690b369a7f87b04c03f4b708" proved="true" expanded="true" shape="ainfix <V0ainfix +aroundaUpV0c1.F">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
</goal>
</theory>
......
examples/bts/12934/why3session.xml
View file @ e4267f5c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="12934/why3session.xml">
<why3session name="bts/12934/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../12934.why" verified="true" expanded="true">
<theory name="BTS12934" verified="true" expanded="true">
<goal name="t" sum="2a75f435f1e835d059a51d852869927a" proved="true" expanded="true">
<goal name="t" sum="2011059e232e4e9d9d6fb53faf2d3bd4" proved="true" expanded="true" shape="t">
<proof prover="coq" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.41"/>
<result status="valid" time="0.44"/>
</proof>
</goal>
</theory>
......
examples/einstein/why3session.xml
View file @ e4267f5c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/einstein/why3session.xml">
<why3session name="./einstein/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../einstein.why" verified="false" expanded="true">
<theory name="Bijection" verified="true" expanded="true">
</theory>
......@@ -9,28 +15,28 @@
<theory name="EinsteinClues" verified="true" expanded="true">
</theory>
<theory name="Goals" verified="false" expanded="true">
<goal name="G1" sum="e98abb6c262bc0761d42df75d5e62c10" proved="true" expanded="true">
<goal name="G1" sum="4e666b5243bdb1064743ec6e271cb8ec" proved="true" expanded="true" shape="ainfix =ato_aFishaGerman">
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal name="Wrong" sum="20fa61f36158b1c59173ef8887200324" proved="false" expanded="true">
<goal name="Wrong" sum="1a0ed387ff3cda5c8323f4eb21fd248c" proved="false" expanded="true" shape="ainfix =ato_aCatsaSwede">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.01"/>
<result status="timeout" time="2.31"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.01"/>
<result status="timeout" time="2.81"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.11"/>
<result status="timeout" time="2.01"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.01"/>
<result status="timeout" time="3.01"/>
</proof>
</goal>
<goal name="G2" sum="3e272e7c2882d425db1cec0218337917" proved="true" expanded="true">
<goal name="G2" sum="44df905be1d95d899616a903f2a08529" proved="true" expanded="true" shape="ainfix =ato_aCatsaNorwegian">
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.08"/>
</proof>
</goal>
</theory>
......
examples/hello_proof/why3session.xml
View file @ e4267f5c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/hello_proof/why3session.xml">
<why3session name="./hello_proof/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../hello_proof.why" verified="false" expanded="true">
<theory name="HelloProof" verified="false" expanded="true">
<goal name="G1" sum="da0794d2f4de035d230d26e93d3e1afe" proved="true" expanded="true" shape="t">
<goal name="G1" sum="b060ede45247709977a2817a7ac6b4bd" proved="true" expanded="true" shape="t">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="07e54d9a25fa3174d5d5bf7ce71a13dc" proved="false" expanded="true" shape="fOtAfIt">
<goal name="G2" sum="29d2b92fcf63e1df963c30f4822b9801" proved="false" expanded="true" shape="fOtAfIt">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="G2.1" sum="f7915ef009bdd949e4af326643583051" proved="false" expanded="true" shape="fIt">
<goal name="G2.1" sum="12fa33a25c8f3a0a042196b8d8c3a85b" proved="false" expanded="true" shape="fIt">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.02"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal name="G2.2" sum="c53f58872dc3cb71805234ace78f1c2d" proved="true" expanded="true" shape="fOt">
<goal name="G2.2" sum="0a8787ba8a8ae75c6e58904fa2a5ece0" proved="true" expanded="true" shape="fOt">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal name="G3" sum="3c319e2d361d8bdd1e51c24c087a2981" proved="true" expanded="true" shape="ainfix >=ainfix *V0V0c0F">
<goal name="G3" sum="957de34bf31dbdb537afc46f3eaaa47b" proved="true" expanded="true" shape="ainfix >=ainfix *V0V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
......
examples/my_cosine/why3session.xml
View file @ e4267f5c
......@@ -2,34 +2,31 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="./my_cosine/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../my_cosine.why" verified="true" expanded="true">
<theory name="CosineSingle" verified="true" expanded="true">
<goal name="MethodError" sum="b6fc96a29dbb1492eab3c9b890206d87" proved="true" expanded="true" shape="ainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix <=aabsV0c0x1.p-5F">
<goal name="MethodError" sum="0332603590a7e267f97b01e0d2291c80" proved="true" expanded="true" shape="ainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix <=aabsV0c0x1.p-5F">
<proof prover="coq" timelimit="2" edited="my_cosine_CosineSingle_MethodError_1.v" obsolete="false">
<result status="valid" time="3.65"/>
<result status="valid" time="4.84"/>
</proof>
</goal>
<goal name="TotalErrorFullyExpanded" sum="762dc642d0fb95fdca3d3ef8644544fd" proved="true" expanded="true" shape="ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix =V3aroundaNearestTiesToEvenainfix -c1.0V2Iainfix =V2aroundaNearestTiesToEvenainfix *c0.5V1Iainfix =V1aroundaNearestTiesToEvenainfix *avalueV0avalueV0FIainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *avalueV0avalueV0acosavalueV0c0x1.p-24Iainfix <=aabsavalueV0c0x1.p-5F">
<goal name="TotalErrorFullyExpanded" sum="bd9ef92a186ff65254c7b2f38940f427" proved="true" expanded="true" shape="ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix =V3aroundaNearestTiesToEvenainfix -c1.0V2Iainfix =V2aroundaNearestTiesToEvenainfix *c0.5V1Iainfix =V1aroundaNearestTiesToEvenainfix *avalueV0avalueV0FIainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *avalueV0avalueV0acosavalueV0c0x1.p-24Iainfix <=aabsavalueV0c0x1.p-5F">
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="TotalErrorExpanded" sum="051b62e81c6bff02e662eeb7a0742164" proved="true" expanded="true" shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<goal name="TotalErrorExpanded" sum="7d92876b865f32fb09dafdaae140429b" proved="true" expanded="true" shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.69"/>
<result status="valid" time="1.27"/>
</proof>
</goal>
<goal name="TotalError" sum="d80467e1b72bec3f873fffec0574b3a7" proved="true" expanded="true" shape="Lacos_singleV0ainfix <=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<goal name="TotalError" sum="0b7eec7fcfb162d6f045cd9836ea76a9" proved="true" expanded="true" shape="Lacos_singleV0ainfix <=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="2.48"/>
<result status="valid" time="4.26"/>
</proof>
</goal>
</theory>
......
examples/programs/assigning_meanings_to_programs/why3session.xml
View file @ e4267f5c
......@@ -2,26 +2,23 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/assigning_meanings_to_programs/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../assigning_meanings_to_programs.mlw" verified="true" expanded="true">
<theory name="WP Sum" verified="true" expanded="true">
<goal name="WP_parameter sum" expl=" parameter sum" sum="fa916cc5e0d85eec4bfc14a054b315d6" proved="true" expanded="true" shape="iainfix <=V4V1ainfix <ainfix -V1V6ainfix -V1V4Aainfix <=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix <=V6ainfix +V1c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix <V4V0Aainfix <=c0V4ainfix =V3asumV2c1ainfix +V1c1Iainfix =V3asumV2c1V4Aainfix <=V4ainfix +V1c1Aainfix <=c1V4FFAainfix =c0asumV2c1c1Aainfix <=c1ainfix +V1c1Aainfix <=c1c1Iainfix <V1V0Aainfix <=c0V1FFF">
<goal name="WP_parameter sum" expl="parameter sum" sum="7fe71cc9d45e92d6cd39abadca465578" proved="true" expanded="true" shape="iainfix <=V4V1ainfix <ainfix -V1V6ainfix -V1V4Aainfix <=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix <=V6ainfix +V1c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix <V4V0Aainfix <=c0V4ainfix =V3asumV2c1ainfix +V1c1Iainfix =V3asumV2c1V4Aainfix <=V4ainfix +V1c1Aainfix <=c1V4FFAainfix =c0asumV2c1c1Aainfix <=c1ainfix +V1c1Aainfix <=c1c1Iainfix <V1V0Aainfix <=c0V1FFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
<theory name="WP Division" verified="true" expanded="true">
<goal name="WP_parameter division" expl=" parameter division" sum="ad4ca868c9bf9e2ed20071557da75449" proved="true" expanded="true" shape="iainfix >=V2V1ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FFAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0FF">
<goal name="WP_parameter division" expl="parameter division" sum="bddcbeb4e7329c77459d020c74ce6e2a" proved="true" expanded="true" shape="iainfix >=V2V1ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FFAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
examples/programs/binary_search/why3session.xml
View file @ e4267f5c
......@@ -2,22 +2,19 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/binary_search/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../binary_search.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter binary_search" expl=" parameter binary_search" sum="45ec37717bb483a53698643fee4a5393" proved="true" expanded="true" shape="iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF">
<goal name="WP_parameter binary_search" expl="parameter binary_search" sum="a0cb3811cc2d2e6a7091476e65c97c65" proved="true" expanded="true" shape="iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
......
examples/programs/bresenham/why3session.xml
View file @ e4267f5c
......@@ -2,78 +2,75 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/bresenham/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../bresenham.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="invariant_is_ok" sum="aea249aa6c35def5f1ab4cc822c59221" proved="true" expanded="true" shape="abestV0V1Iainvariant_V0V1V2F">
<goal name="invariant_is_ok" sum="4d1b7b29d42a26ab5c6d98ec1dfed40c" proved="true" expanded="true" shape="abestV0V1Iainvariant_V0V1V2F">
<proof prover="coq" timelimit="10" edited="bresenham_WP_M_invariant_is_ok_1.v" obsolete="false">
<result status="valid" time="1.22"/>
<result status="valid" time="1.58"/>
</proof>
</goal>
<goal name="WP_parameter bresenham" expl=" parameter bresenham" sum="5f519ef1874e86cf7ab8d7e7fe744a24" proved="true" expanded="true" shape="iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFFAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<goal name="WP_parameter bresenham" expl="parameter bresenham" sum="5fbf0d989772686895987cce35b013c5" proved="true" expanded="true" shape="iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFFAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter bresenham.1" expl="loop invariant init" sum="9968895e2cd7366a98c49572320a0dcc" proved="true" expanded="true" shape="ainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<goal name="WP_parameter bresenham.1" expl="loop invariant init" sum="f3884b27cd04132a76bb13d18ae42cf5" proved="true" expanded="true" shape="ainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.04"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.2" expl="assertion" sum="b45fbde1ba425ad1281f0555990c5998" proved="true" expanded="true" shape="abestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.2" expl="assertion" sum="f8200ef59145ee8ca8295c3fa1d9b330" proved="true" expanded="true" shape="abestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.20"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.3" expl="loop invariant preservation" sum="5298a9d98e3360d62ca7cd2ba3735a46" proved="true" expanded="true" shape="ainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.3" expl="loop invariant preservation" sum="8e10024cda416e79b6fa069ac98d34c0" proved="true" expanded="true" shape="ainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.4" expl="loop variant decreases" sum="e5242a8ea4c12ecaf496faeaf8781ba3" proved="true" expanded="true" shape="ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.4" expl="loop variant decreases" sum="314d3a2fb7cbfc509c9bb8e7825a0e13" proved="true" expanded="true" shape="ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.5" expl="loop invariant preservation" sum="c06e9e75447e9ded9275160e93e3791a" proved="true" expanded="true" shape="ainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.5" expl="loop invariant preservation" sum="c64d26f7408067cc3375373dc8e54cb6" proved="true" expanded="true" shape="ainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.6" expl="loop variant decreases" sum="37430f262a395cdbbe02f14faa1fc542" proved="true" expanded="true" shape="ainfix <ainfix -ainfix +ax2c1V5ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.6" expl="loop variant decreases" sum="98ce37cd1d9a39aaf0e6ed47cb674f2a" proved="true" expanded="true" shape="ainfix <ainfix -ainfix +ax2c1V5ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
......
examples/programs/checking_a_large_routine/why3session.xml
View file @ e4267f5c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="checking_a_large_routine/why3session.xml">
<why3session name="programs/checking_a_large_routine/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
......@@ -9,65 +9,65 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../checking_a_large_routine.mlw" verified="true" expanded="true">
<theory name="WP CheckingALargeRoutine" verified="true" expanded="true">
<goal name="WP_parameter routine" expl="parameter routine" sum="5b264b1ffef9b0cf942d6a26937d1e6c" proved="true" expanded="true" shape="iainfix <V2V0iainfix <=V3V2ainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1Fainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =V4afactV7Aainfix <=V7V0Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFAainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1ainfix =V1afactV0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFAainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F">
<goal name="WP_parameter routine" expl="parameter routine" sum="64e0aa055e160c153c91bd7ae8ce40e8" proved="true" expanded="true" shape="iainfix <V2V0iainfix <=V3V2ainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1Fainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =V4afactV7Aainfix <=V7V0Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFAainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1ainfix =V1afactV0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFAainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter routine.1" expl="loop invariant init" sum="698d7153b292aa8e6d44bc62e6288882" proved="true" expanded="true" shape="ainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F">
<goal name="WP_parameter routine.1" expl="loop invariant init" sum="451b17060104739c7e34cf3dcd8e97d9" proved="true" expanded="true" shape="ainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter routine.2" expl="loop invariant init" sum="2c1435fb10b7e50dbaa36b1d275d4ca7" proved="true" expanded="true" shape="ainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<goal name="WP_parameter routine.2" expl="loop invariant init" sum="150db32199706232f26823937ab3c138" proved="true" expanded="true" shape="ainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter routine.3" expl="loop invariant preservation" sum="5f308a9408cb2e091e140542fbf7b738" proved="true" expanded="true" shape="ainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<goal name="WP_parameter routine.3" expl="loop invariant preservation" sum="27427b58be039f71fd64654674d2c56e" proved="true" expanded="true" shape="ainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter routine.4" expl="loop variant decreases" sum="1dd48d2368d5d8c64e6807b76ba466e7" proved="true" expanded="true" shape="ainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Iainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<goal name="WP_parameter routine.4" expl="loop variant decreases" sum="b0f30da25de40b52bfaa27eda2c4054c" proved="true" expanded="true" shape="ainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Iainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter routine.5" expl="loop invariant preservation" sum="be92a4d050ec0edd72b34c9e4e18a3ed" proved="true" expanded="true" shape="ainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix <=V3V2NIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<goal name="WP_parameter routine.5" expl="loop invariant preservation" sum="a421b793d3bb3a814cf21aa982abe208" proved="true" expanded="true" shape="ainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix <=V3V2NIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter routine.6" expl="loop variant decreases" sum="c3a241c53ef9ce60948ed2333f33bf1c" proved="true" expanded="true" shape="ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix <=V3V2NIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<goal name="WP_parameter routine.6" expl="loop variant decreases" sum="72258ae62802b736d8cf52092e97bcb0" proved="true" expanded="true" shape="ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix <=V3V2NIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter routine.7" expl="normal postcondition" sum="0c9c877516ed94fa9e9a4bbf23ab2133" proved="true" expanded="true" shape="ainfix =V1afactV0Iainfix <V2V0NIainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<goal name="WP_parameter routine.7" expl="normal postcondition" sum="70c6767fa0d10d226c32cdc92d1a9883" proved="true" expanded="true" shape="ainfix =V1afactV0Iainfix <V2V0NIainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter routine2" expl="parameter routine2" sum="eee978067219a2a7176850cb4a8d5f91" proved="true" expanded="true" shape="ainfix =V1afactV0Iainfix =V1afactainfix +ainfix -V0c1c1Aainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFAainfix =c1afactc0Iainfix <=c0ainfix -V0c1Aainfix =c1afactV0Iainfix >c0ainfix -V0c1Iainfix >=V0c0F">
<goal name="WP_parameter routine2" expl="parameter routine2" sum="b9cc91755efe956ec4134c3c369d2a1f" proved="true" expanded="true" shape="ainfix =V1afactV0Iainfix =V1afactainfix +ainfix -V0c1c1Aainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFAainfix =c1afactc0Iainfix <=c0ainfix -V0c1Aainfix =c1afactV0Iainfix >c0ainfix -V0c1Iainfix >=V0c0F">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter routine2.1" expl="normal postcondition" sum="438b099822fcddbd06e418a6302af2b1" proved="true" expanded="true" shape="ainfix =c1afactV0Iainfix >c0ainfix -V0c1Iainfix >=V0c0F">
<goal name="WP_parameter routine2.1" expl="normal postcondition" sum="fdb9fb760a56ab5daa224bcf1cdd0a04" proved="true" expanded="true" shape="ainfix =c1afactV0Iainfix >c0ainfix -V0c1Iainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter routine2.2" expl="for loop initialization" sum="dde2dd81eef80b4e2df04cfe2aaa6565" proved="true" expanded="true" shape="ainfix =c1afactc0Iainfix <=c0ainfix -V0c1Iainfix >=V0c0F">
<goal name="WP_parameter routine2.2" expl="for loop initialization" sum="8e26b24e4cef9f1c4b16879dba391baf" proved="true" expanded="true" shape="ainfix =c1afactc0Iainfix <=c0ainfix -V0c1Iainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter routine2.3" expl="for loop preservation" sum="c6d48580e9f8dd881f5d59d1fa001157" proved="true" expanded="true" shape="ainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix >=V0c0F">
<goal name="WP_parameter routine2.3" expl="for loop preservation" sum="68c61544e0578a27704a22c102a75ea2" proved="true" expanded="true" shape="ainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter routine2.4" expl="normal postcondition" sum="609eb9f3cf703de6155a3a9fb3b8719d" proved="true" expanded="true" shape="ainfix =V1afactV0Iainfix =V1afactainfix +ainfix -V0c1c1FIainfix <=c0ainfix -V0c1Iainfix >=V0c0F">
<goal name="WP_parameter routine2.4" expl="normal postcondition" sum="b028922fd7ef6faef89a149d15fa56e8" proved="true" expanded="true" shape="ainfix =V1afactV0Iainfix =V1afactainfix +ainfix -V0c1c1FIainfix <=c0ainfix -V0c1Iainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</transf>
......
examples/programs/decrease1/why3session.xml
View file @ e4267f5c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/decrease1/why3session.xml">
<why3session name="programs/decrease1/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../decrease1.mlw" verified="true" expanded="true">
<theory name="WP Decrease1" verified="true" expanded="true">
<goal name="decrease1_induction" sum="9663d3d345fd283056aa58595056841f" proved="true" expanded="true" shape="ainfix >=amixfix []V0V2ainfix -ainfix +amixfix []V0V1V1V2Iainfix <V2alengthV0Aainfix <=V1V2Aainfix <=c0V1FIadecrease1V0F">
<goal name="decrease1_induction" sum="0b5a5fde45e86c1bc677f99c692e19db" proved="true" expanded="true" shape="ainfix >=amixfix []V0V2ainfix -ainfix +amixfix []V0V1V1V2Iainfix <V2alengthV0Aainfix <=V1V2Aainfix <=c0V1FIadecrease1V0F">
<proof prover="coq" timelimit="10" edited="decrease1_Decrease1_decrease1_induction_2.v" obsolete="false">
<result status="valid" time="0.60"/>
<result status="valid" time="0.89"/>
</proof>
</goal>
<goal name="WP_parameter search" expl="parameter search" sum="8fd534f9e23b388e09448b767c337195" proved="true" expanded="true" shape="iainfix <V2V0iainfix =agetV1V2c0ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1iainfix >agetV1V2c0ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V6c0NIainfix <V6V0Iainfix <V6V5Aainfix <=c0V6FAainfix <=c0V5Iainfix =V5ainfix +V2agetV1V2FAainfix <V2V0Aainfix <=c0V2ainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V8c0NIainfix <V8V0Iainfix <V8V7Aainfix <=c0V8FAainfix <=c0V7Iainfix =V7ainfix +V2c1FAainfix <V2V0Aainfix <=c0V2Aainfix <V2V0Aainfix <=c0V2ainfix =agetV1V9c0NIainfix <V9aprefix -c1Aainfix <=c0V9FAainfix =agetV1aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=c0aprefix -c1Oainfix =agetV1V10c0NIainfix <V10V0Aainfix <=c0V10FAainfix =aprefix -c1aprefix -c1Iainfix =agetV1V11c0NIainfix <V11V0Iainfix <V11V2Aainfix <=c0V11FAainfix <=c0V2FAainfix =agetV1V12c0NIainfix <V12V0Iainfix <V12c0Aainfix <=c0V12FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
<goal name="WP_parameter search" expl="parameter search" sum="32db91f9d0b74d7901921f96c785e138" proved="true" expanded="true" shape="iainfix <V2V0iainfix =agetV1V2c0ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1iainfix >agetV1V2c0ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V6c0NIainfix <V6V0Iainfix <V6V5Aainfix <=c0V6FAainfix <=c0V5Iainfix =V5ainfix +V2agetV1V2FAainfix <V2V0Aainfix <=c0V2ainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V8c0NIainfix <V8V0Iainfix <V8V7Aainfix <=c0V8FAainfix <=c0V7Iainfix =V7ainfix +V2c1FAainfix <V2V0Aainfix <=c0V2Aainfix <V2V0Aainfix <=c0V2ainfix =agetV1V9c0NIainfix <V9aprefix -c1Aainfix <=c0V9FAainfix =agetV1aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=c0aprefix -c1Oainfix =agetV1V10c0NIainfix <V10V0Aainfix <=c0V10FAainfix =aprefix -c1aprefix -c1Iainfix =agetV1V11c0NIainfix <V11V0Iainfix <V11V2Aainfix <=c0V11FAainfix <=c0V2FAainfix =agetV1V12c0NIainfix <V12V0Iainfix <V12c0Aainfix <=c0V12FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter search.1" expl="loop invariant init" sum="bcf8c81ba18b978a3ab6d782d6b80c57" proved="true" expanded="true" shape="ainfix =agetV1V2c0NIainfix <V2V0Iainfix <V2c0Aainfix <=c0V2FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
<goal name="WP_parameter search.1" expl="loop invariant init" sum="f429462d6359f2a28844ffc1a8f1eec0" proved="true" expanded="true" shape="ainfix =agetV1V2c0NIainfix <V2V0Iainfix <V2c0Aainfix <=c0V2FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter search.2" expl="precondition" sum="57f1612854871fa1ae27dc629318415e" proved="true" expanded="true" shape="ainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
<goal name="WP_parameter search.2" expl="precondition" sum="00f49e69817e47e187436aba2e90adce" proved="true" expanded="true" shape="ainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter search.3" expl="normal postcondition" sum="13963d89bde79ce4e5d1f0dc219c83b2" proved="true" expanded="true" shape="ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1Iainfix =agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
<goal name="WP_parameter search.3" expl="normal postcondition" sum="1f5739e3fba1f66944af9f0ce685a8af" proved="true" expanded="true" shape="ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1Iainfix =agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter search.4" expl="precondition" sum="5bf225d3fdf0d3dc78b90f30a7b987fe" proved="true" expanded="true" shape="ainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
<goal name="WP_parameter search.4" expl="precondition" sum="95604080b163273becaafe2a7359ed70" proved="true" expanded="true" shape="ainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter search.5" expl="precondition" sum="e41c52ffcae88b8c341592cc7318e7bc" proved="true" expanded="true" shape="ainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
<goal name="WP_parameter search.5" expl="precondition" sum=