Commit bbb659aa authored by MARCHE Claude's avatar MARCHE Claude

updated example isqrt

parent 94223ac7
......@@ -33,7 +33,9 @@ module Simple
= let count = ref 0 in
let sum = ref 1 in
while !sum <= x do
invariant { !count >= 0 /\ x >= sqr !count /\ !sum = sqr (!count+1) }
invariant { !count >= 0 }
invariant { x >= sqr !count }
invariant { !sum = sqr (!count+1) }
variant { x - !count }
count := !count + 1;
sum := !sum + 2 * !count + 1
......@@ -72,19 +74,20 @@ module NewtonMethod
y := !z;
z := div (div x !z + !z) 2;
(* A few hints to prove preservation of the last invariant *)
let ghost a = div x !y in
assert { x < a * !y + !y };
assert { a + !y <= 2 * !z + 1 };
assert { 0 <= a + !y + 1 };
assert { sqr (a + !y + 1) <= sqr (2 * !z + 2) };
assert { 4 * (sqr (!z + 1) - x)
assert { x < sqr (!z + 1)
by let a = div x !y in
x < a * !y + !y
so a + !y <= 2 * !z + 1
so sqr (a + !y + 1) <= sqr (2 * !z + 2)
so 4 * (sqr (!z + 1) - x)
= sqr (2 * !z + 2) - 4 * x
>= sqr (a + !y + 1) - 4 * x
> sqr (a + !y + 1) - 4 * (a * !y + !y)
= sqr (a + 1 - !y)
>= 0 }
done;
assert { !y * !y <= div x !y * !y by !y <= div x !y };
assert { !y * !y <= div x !y * !y
by !y <= div x !y };
!y
end
......@@ -3,33 +3,45 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="1" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="7" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="1" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../isqrt.mlw" expanded="true">
<theory name="Square" sum="9d10f7a99e3dc8b97241d913352efc97">
<theory name="Square" sum="9d10f7a99e3dc8b97241d913352efc97" expanded="true">
<goal name="sqr_non_neg">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="sqr_increasing">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="1" timelimit="5" memlimit="4000"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sqr_sum">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
</theory>
<theory name="Simple" sum="b9231cbba4db342a3e2006fe92f14e06">
<theory name="Simple" sum="ac5c609b139dc287f99fc9e57f1648fc" expanded="true">
<goal name="WP_parameter isqrt" expl="VC for isqrt">
<transf name="split_goal_wp">
<goal name="WP_parameter isqrt.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt.2" expl="2. loop invariant init">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt.3" expl="3. loop invariant init">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt.4" expl="4. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt.2" expl="2. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.00" steps="15"/></proof>
<goal name="WP_parameter isqrt.5" expl="5. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt.6" expl="6. loop invariant preservation">
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
<goal name="WP_parameter isqrt.3" expl="3. loop variant decrease">
<goal name="WP_parameter isqrt.7" expl="7. loop variant decrease">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter isqrt.4" expl="4. postcondition">
<goal name="WP_parameter isqrt.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
......@@ -38,9 +50,9 @@
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</theory>
<theory name="NewtonMethod" sum="963cc5da969d37ed9834dacc348651ec">
<goal name="WP_parameter sqrt" expl="VC for sqrt">
<transf name="split_goal_wp">
<theory name="NewtonMethod" sum="4c49ea3ad1eb6ebc2d9c7e9e4c20c7d3" expanded="true">
<goal name="WP_parameter sqrt" expl="VC for sqrt" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter sqrt.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
......@@ -54,7 +66,7 @@
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter sqrt.5" expl="5. loop invariant init">
<proof prover="1"><result status="valid" time="1.21"/></proof>
<proof prover="1" timelimit="5" memlimit="4000"><result status="valid" time="1.21"/></proof>
</goal>
<goal name="WP_parameter sqrt.6" expl="6. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
......@@ -63,51 +75,67 @@
<proof prover="0"><result status="valid" time="0.03" steps="12"/></proof>
</goal>
<goal name="WP_parameter sqrt.8" expl="8. assertion">
<proof prover="7"><result status="valid" time="0.01"/></proof>
<transf name="split_goal_wp">
<goal name="WP_parameter sqrt.8.1" expl="1. VC for sqrt">
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.2" expl="2. VC for sqrt">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.3" expl="3. VC for sqrt">
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.4" expl="4. VC for sqrt">
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.5" expl="5. VC for sqrt">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.6" expl="6. VC for sqrt">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.7" expl="7. VC for sqrt">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.8" expl="8. VC for sqrt">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.8.9" expl="9. VC for sqrt">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sqrt.9" expl="9. assertion">
<proof prover="7"><result status="valid" time="0.02"/></proof>
<goal name="WP_parameter sqrt.9" expl="9. loop invariant preservation">
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter sqrt.10" expl="10. assertion">
<proof prover="7"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter sqrt.10" expl="10. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.11" expl="11. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<goal name="WP_parameter sqrt.11" expl="11. loop invariant preservation">
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter sqrt.12" expl="12. assertion">
<proof prover="0"><result status="valid" time="0.06" steps="20"/></proof>
<goal name="WP_parameter sqrt.12" expl="12. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.13" expl="13. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.09" steps="21"/></proof>
</goal>
<goal name="WP_parameter sqrt.14" expl="14. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter sqrt.15" expl="15. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter sqrt.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter sqrt.17" expl="17. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sqrt.18" expl="18. loop variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
<goal name="WP_parameter sqrt.14" expl="14. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sqrt.19" expl="19. assertion">
<goal name="WP_parameter sqrt.15" expl="15. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter sqrt.19.1" expl="1. VC for sqrt">
<proof prover="7"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter sqrt.15.1" expl="1. VC for sqrt">
<proof prover="7" timelimit="5" memlimit="4000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter sqrt.19.2" expl="2. VC for sqrt">
<goal name="WP_parameter sqrt.15.2" expl="2. VC for sqrt">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sqrt.20" expl="20. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter sqrt.16" expl="16. postcondition">
<proof prover="1" timelimit="5" memlimit="4000"><result status="valid" time="0.01"/></proof>
<proof prover="7" timelimit="5" memlimit="4000"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</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