verifythis 2015, challenge 1: simplification

parent eab93a08
...@@ -126,7 +126,6 @@ module RelaxedPrefix ...@@ -126,7 +126,6 @@ module RelaxedPrefix
let ghost ignored = ref 0 in let ghost ignored = ref 0 in
for i = 0 to n - 1 do for i = 0 to n - 1 do
invariant { 0 <= !shift <= 1 } invariant { 0 <= !shift <= 1 }
invariant { i = 0 -> !shift = 0 }
invariant { !shift = 1 -> 0 <= !ignored < i } invariant { !shift = 1 -> 0 <= !ignored < i }
invariant { m + !shift >= i } invariant { m + !shift >= i }
invariant { invariant {
......
...@@ -4,107 +4,98 @@ ...@@ -4,107 +4,98 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/> <prover id="2" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<file name="../verifythis_2015_relaxed_prefix.mlw"> <file name="../verifythis_2015_relaxed_prefix.mlw" expanded="true">
<theory name="RelaxedPrefix" sum="1aec45f1cb638f259a0aa093f19178a1"> <theory name="RelaxedPrefix" sum="64ae97234d56ce75d88590b835d579a3" expanded="true">
<goal name="WP_parameter is_relaxed_prefix" expl="VC for is_relaxed_prefix"> <goal name="WP_parameter is_relaxed_prefix" expl="VC for is_relaxed_prefix" expanded="true">
<transf name="split_goal_wp"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter is_relaxed_prefix.1" expl="1. postcondition"> <goal name="WP_parameter is_relaxed_prefix.1" expl="1. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.2" expl="2. loop invariant init"> <goal name="WP_parameter is_relaxed_prefix.2" expl="2. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.3" expl="3. loop invariant init"> <goal name="WP_parameter is_relaxed_prefix.3" expl="3. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.4" expl="4. loop invariant init"> <goal name="WP_parameter is_relaxed_prefix.4" expl="4. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.5" expl="5. loop invariant init"> <goal name="WP_parameter is_relaxed_prefix.5" expl="5. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.6" expl="6. postcondition"> <goal name="WP_parameter is_relaxed_prefix.6" expl="6. postcondition" expanded="true">
<transf name="inline_goal"> <transf name="inline_goal" expanded="true">
<goal name="WP_parameter is_relaxed_prefix.6.1" expl="1. postcondition"> <goal name="WP_parameter is_relaxed_prefix.6.1" expl="1. postcondition" expanded="true">
<transf name="split_goal_wp"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter is_relaxed_prefix.6.1.1" expl="1. postcondition"> <goal name="WP_parameter is_relaxed_prefix.6.1.1" expl="1. postcondition" expanded="true">
<proof prover="0" timelimit="30"><result status="valid" time="0.02" steps="11"/></proof> <proof prover="0" timelimit="30"><result status="valid" time="0.02" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.6.1.2" expl="2. postcondition"> <goal name="WP_parameter is_relaxed_prefix.6.1.2" expl="2. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.03" steps="14"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="12"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.7" expl="7. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.7" expl="7. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.8" expl="8. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.8" expl="8. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.9" expl="9. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.9" expl="9. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter is_relaxed_prefix.10" expl="10. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.11" expl="11. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.10" expl="10. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.15" steps="43"/></proof> <proof prover="0"><result status="valid" time="0.15" steps="43"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.12" expl="12. index in array bounds"> <goal name="WP_parameter is_relaxed_prefix.11" expl="11. index in array bounds" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.13" expl="13. index in array bounds"> <goal name="WP_parameter is_relaxed_prefix.12" expl="12. index in array bounds" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.14" expl="14. postcondition"> <goal name="WP_parameter is_relaxed_prefix.13" expl="13. postcondition" expanded="true">
<transf name="inline_goal"> <transf name="inline_goal" expanded="true">
<goal name="WP_parameter is_relaxed_prefix.14.1" expl="1. postcondition"> <goal name="WP_parameter is_relaxed_prefix.13.1" expl="1. postcondition" expanded="true">
<transf name="split_goal_wp"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter is_relaxed_prefix.14.1.1" expl="1. postcondition"> <goal name="WP_parameter is_relaxed_prefix.13.1.1" expl="1. postcondition" expanded="true">
<proof prover="0" timelimit="30"><result status="valid" time="0.03" steps="34"/></proof> <proof prover="0" timelimit="30"><result status="valid" time="0.03" steps="90"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.14.1.2" expl="2. postcondition"> <goal name="WP_parameter is_relaxed_prefix.13.1.2" expl="2. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.31" steps="353"/></proof> <proof prover="0"><result status="valid" time="0.31" steps="351"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.15" expl="15. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.14" expl="14. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.16" expl="16. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.15" expl="15. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter is_relaxed_prefix.17" expl="17. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.18" expl="18. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.16" expl="16. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.19" expl="19. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.17" expl="17. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.10" steps="77"/></proof> <proof prover="0"><result status="valid" time="0.10" steps="77"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.20" expl="20. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.18" expl="18. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.21" expl="21. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.19" expl="19. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter is_relaxed_prefix.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.23" expl="23. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.20" expl="20. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.24" expl="24. loop invariant preservation"> <goal name="WP_parameter is_relaxed_prefix.21" expl="21. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.08" steps="157"/></proof> <proof prover="0"><result status="valid" time="0.08" steps="153"/></proof>
</goal> </goal>
<goal name="WP_parameter is_relaxed_prefix.25" expl="25. postcondition"> <goal name="WP_parameter is_relaxed_prefix.22" expl="22. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="38"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="36"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
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