Commit 342f7914 authored by MARCHE Claude's avatar MARCHE Claude

sessions files appropriate for moloch

parent 6ce9d548
......@@ -4,20 +4,11 @@
<file name="../decrease1.mlw" verified="true" expanded="true">
<theory name="Decrease1" verified="true" expanded="true">
<goal name="decrease1_induction" sum="8319c3299f6c5b391aec5943ca151429" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="examples/programs/decrease1/decrease1.mlw_Decrease1_decrease1_induction_2.v" obsolete="false">
<proof prover="coq" timelimit="10" edited="decrease1.mlw_Decrease1_decrease1_induction_2.v" obsolete="false">
<result status="valid" time="0.75"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.45"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.12"/>
</proof>
</goal>
<goal name="WP_parameter search" expl="correctness of parameter search" sum="46e3d9215dcd11606cc49de64a5a327f" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.08"/>
</proof>
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter search.1" expl="loop invariant init" sum="f5954e0aa354b70603e2561453b4ded0" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
......@@ -60,9 +51,6 @@
</proof>
</goal>
<goal name="WP_parameter search.6" expl="loop invariant preservation" sum="f4703704714fb12b1cfc7e1f7033703a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="examples/programs/decrease1/decrease1.mlw-Decrease1-WP_parameter search_1.why" obsolete="false"><undone/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.10"/>
</proof>
......@@ -102,9 +90,6 @@
</transf>
</goal>
<goal name="WP_parameter search_rec" expl="correctness of parameter search_rec" sum="9fb29a60c6f5cf8d6b537c46b8c3ba87" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.17"/>
</proof>
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter search_rec.1" expl="precondition" sum="e99d8b29c61d5561f42de7428f854f98" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
......@@ -147,9 +132,6 @@
</proof>
</goal>
<goal name="WP_parameter search_rec.6" expl="normal postcondition" sum="66a382fecdcc926c2651f0df8b934922" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.09"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.24"/>
</proof>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/gcd_bezout/why3session.xml">
<why3session name="examples/programs/gcd_bezout/why3session.xml">
<file name="../gcd_bezout.mlw" verified="false" expanded="true">
<theory name="M" verified="false" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="44c73ab6d7cb8f3f8241f534deb156f1" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="highfailure" time="0.30"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter gcd.1" expl="loop invariant init" sum="8566a02a986fda736b7f696339e845f1" proved="true" expanded="false">
<goal name="WP_parameter gcd.1" expl="loop invariant init" sum="8566a02a986fda736b7f696339e845f1" proved="true" expanded="true">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
......@@ -32,46 +20,61 @@
</proof>
</goal>
<goal name="WP_parameter gcd.2" expl="loop invariant preservation" sum="6aa9c41319e3ce9cdb5c07f21e43fc1a" proved="false" expanded="true">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.06"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.11"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter gcd.2.1" expl="correctness of parameter gcd" sum="2bf2b9018cef97e7d6861be9a099632c" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.2" expl="correctness of parameter gcd" sum="134839062fcb2bdd8f91686991426f7d" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.3" expl="correctness of parameter gcd" sum="77ed7e7e438dca7dc5d795505d376a85" proved="false" expanded="true">
<proof prover="simplify" timelimit="3" edited="" obsolete="false">
<result status="timeout" time="3.09"/>
</proof>
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="timeout" time="3.08"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
</proof>
<proof prover="z3" timelimit="3" edited="" obsolete="false">
<result status="timeout" time="3.08"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.4" expl="correctness of parameter gcd" sum="1221b85597e3a6d4bbdb929662515a1b" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.5" expl="correctness of parameter gcd" sum="dd8408987193bff8e40272015be1aa9d" proved="true" expanded="true">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter gcd.3" expl="loop variant decreases" sum="cca2a902409976d7fe1249041e32fc6e" proved="true" expanded="false">
<goal name="WP_parameter gcd.3" expl="loop variant decreases" sum="cca2a902409976d7fe1249041e32fc6e" proved="true" expanded="true">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.09"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter gcd.4" expl="normal postcondition" sum="70282398b1f17ace6b7f8ea5e5755ba1" proved="true" expanded="false">
<goal name="WP_parameter gcd.4" expl="normal postcondition" sum="70282398b1f17ace6b7f8ea5e5755ba1" proved="true" expanded="true">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.72"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="1.14"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
</goal>
</transf>
</goal>
......
......@@ -2,14 +2,11 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/power/why3session.xml">
<file name="../power.mlw" verified="false" expanded="true">
<theory name="Power" verified="true" expanded="true">
<theory name="Power" verified="true" expanded="false">
<goal name="Power_1" sum="1db7c130e0faaa3525077846831aadf3" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
......@@ -17,69 +14,74 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="Power_sum" sum="0222179599018e583f47a3d214f2e604" proved="true" expanded="true">
<goal name="Power_sum" sum="0222179599018e583f47a3d214f2e604" proved="true" expanded="false">
<proof prover="coq" timelimit="2" edited="power.mlw_Power_Power_sum_1.v" obsolete="false">
<result status="valid" time="0.46"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.07"/>
</proof>
</goal>
<goal name="Power_mult" sum="9d09d633adb75294ad19c24d7ad24bf4" proved="true" expanded="false">
<proof prover="coq" timelimit="2" edited="power.mlw_Power_Power_mult_1.v" obsolete="false">
<result status="valid" time="0.52"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="1.50"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.15"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
</goal>
</theory>
<theory name="M" verified="false" expanded="true">
<goal name="WP_parameter fast_exp" expl="correctness of parameter fast_exp" sum="ff0a5f4d7ce2252d7f09664075c560a8" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.10"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative" expl="correctness of parameter fast_exp_imperative" sum="22f72b816b6021c98b7d03397cb1d7fd" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.00"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter fast_exp_imperative.1" expl="loop invariant init" sum="0bac504113a8f4e466cd5612d00220fa" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.2" expl="loop invariant preservation" sum="5117e72c11ee204306335e1da3b9a5e7" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.3" expl="loop variant decreases" sum="80be8265c76399ff1ed013b560c05ac9" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.4" expl="loop invariant preservation" sum="0c03c29f50e52bd5961ca54bd12cf4b9" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter fast_exp_imperative.4.1" expl="correctness of parameter fast_exp_imperative" sum="7ab6e51299cce66c2e5f2754452a91db" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.4.2" expl="correctness of parameter fast_exp_imperative" sum="153686c76ecf6d6a9fa404474076db03" proved="false" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="7.32"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fast_exp_imperative.5" expl="loop variant decreases" sum="747a9ee60c2446165c15c68a77f30fa3" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.6" expl="normal postcondition" sum="5b3b282549aa378cfe6033b144badb05" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment