Commit 29968f21 authored by MARCHE Claude's avatar MARCHE Claude

example mccarthy, with version using fast WP

parent 8e710b9a
......@@ -2,55 +2,41 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Z3" version="3.2" timelimit="10" memlimit="0"/>
<prover id="3" name="veriT" version="201310" timelimit="5" memlimit="4000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../mccarthy.mlw" expanded="true">
<theory name="McCarthy91" sum="3b0127c736e128044619dfecbc3474f5" expanded="true">
<goal name="WP_parameter f91" expl="VC for f91" expanded="true">
<proof prover="0" timelimit="2"><result status="valid" time="0.00"/></proof>
<proof prover="1" timelimit="2"><result status="valid" time="0.02"/></proof>
<proof prover="2" timelimit="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<theory name="McCarthy91" sum="dfd70d690529e1a36626f39ca1116ffb" expanded="true">
<goal name="VC f91" expl="VC for f91" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC f91.1" expl="1. variant decrease">
<proof prover="4"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="VC f91.2" expl="2. variant decrease">
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="VC f91.3" expl="3. postcondition">
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter f91_nonrec" expl="VC for f91_nonrec" expanded="true">
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter f91_nonrec.1" expl="1. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.2" expl="2. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.3" expl="3. loop variant decrease" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.4" expl="4. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.5" expl="5. loop variant decrease" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f91_nonrec.6" expl="6. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<goal name="VC f91_nonrec.1" expl="1. loop invariant init">
<proof prover="4"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="VC f91_nonrec.2" expl="2. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.03" steps="46"/></proof>
</goal>
<goal name="VC f91_nonrec.3" expl="3. loop variant decrease">
<proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC f91_nonrec.4" expl="4. loop invariant preservation">
<proof prover="4"><result status="valid" time="1.32" steps="222"/></proof>
</goal>
<goal name="VC f91_nonrec.5" expl="5. loop variant decrease">
<proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC f91_nonrec.6" expl="6. postcondition">
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</transf>
</goal>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../mccarthy.mlw" expanded="true">
<theory name="McCarthy91" sum="d0ab9c573ee2fb06c1965f930c12cf9f" expanded="true">
<goal name="VC f91" expl="VC for f91" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC f91.1" expl="1. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="VC f91.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC f91.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
</transf>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC f91_nonrec.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="VC f91_nonrec.2" expl="2. loop invariant preservation">
<proof prover="0"><result status="valid" time="1.01" steps="255"/></proof>
</goal>
<goal name="VC f91_nonrec.3" expl="3. loop variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC f91_nonrec.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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