Sieve of Eratosthenes slightly improved

parent 7b0513b1
(** Sieve of Eratosthenes
Author: Martin Clochard
See also knuth_prime_numbers.mlw in the gallery.
*)
module Sieve
use import int.Int
use import array.Array
use import ref.Ref
use import number.Prime
predicate no_factor_lt (bnd num:int) =
num > 1 /\ forall k l. 1 < l < bnd /\ k > 1 -> num <> k * l
......@@ -25,15 +33,17 @@ module Sieve
invariant { forall j. 0 <= j < n -> t[j] <-> no_factor_lt !i j }
variant { n - !i }
if t[!i] then begin
let r = ref !i in
while !r * !i < n do
invariant { 1 < !r <= n }
let s = ref (!i * !i) in
let ghost r = ref !i in
while !s < n do
invariant { 1 < !r <= n /\ !s = !r * !i }
invariant { forall j. 0 <= j < n ->
t[j] <-> (no_factor_lt !i j /\
forall k. 1 < k < !r -> j <> k * !i) }
variant { n - !r }
t[!r * !i] <- false;
incr r;
t[!s] <- false;
s := !s + !i;
incr r
done;
assert { forall j. 0 <= j < n /\ t[j] ->
(forall k l. 1 < l < !i + 1 -> j = k * l /\ k > 1 ->
......@@ -50,6 +60,6 @@ module Sieve
assert { forall j. 0 <= j < n /\ prime j ->
forall k l. 1 < l < n /\ k > 1 -> j = k * l -> l >= j && false };
t
end
......@@ -4,14 +4,16 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="6" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="6" memlimit="1000"/>
<prover id="5" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<file name="../eratosthene.mlw" expanded="true">
<theory name="Sieve" sum="a84c73b798e84f0d280c74dcdb167347" expanded="true">
<theory name="Sieve" sum="ab6af832e3940061fcfb751a7949a19d" expanded="true">
<goal name="WP_parameter incr" expl="VC for incr">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="WP_parameter sieve" expl="VC for sieve">
<transf name="split_goal_wp">
<goal name="WP_parameter sieve" expl="VC for sieve" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter sieve.1" expl="1. array creation size">
<proof prover="0"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
......@@ -40,47 +42,57 @@
<proof prover="5"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter sieve.10" expl="10. type invariant">
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter sieve.11" expl="11. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter sieve.12" expl="12. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<transf name="split_goal_wp">
<goal name="WP_parameter sieve.12.1" expl="1. VC for sieve">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sieve.12.2" expl="2. VC for sieve">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter sieve.12.3" expl="3. VC for sieve">
<proof prover="0" timelimit="6"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sieve.13" expl="13. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.17" steps="85"/></proof>
<proof prover="0"><result status="valid" time="0.37" steps="87"/></proof>
</goal>
<goal name="WP_parameter sieve.14" expl="14. loop variant decrease">
<proof prover="0"><result status="valid" time="0.04" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="23"/></proof>
</goal>
<goal name="WP_parameter sieve.15" expl="15. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter sieve.15.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.69" steps="77"/></proof>
<proof prover="0"><result status="valid" time="0.52" steps="78"/></proof>
</goal>
<goal name="WP_parameter sieve.15.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="41"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="WP_parameter sieve.15.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.86" steps="77"/></proof>
<proof prover="0"><result status="valid" time="0.86" steps="78"/></proof>
</goal>
<goal name="WP_parameter sieve.15.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.03" steps="25"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="26"/></proof>
</goal>
<goal name="WP_parameter sieve.15.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.05" steps="59"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="60"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sieve.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="WP_parameter sieve.17" expl="17. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.15" steps="70"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="71"/></proof>
</goal>
<goal name="WP_parameter sieve.18" expl="18. loop variant decrease">
<proof prover="0"><result status="valid" time="0.03" steps="19"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="20"/></proof>
</goal>
<goal name="WP_parameter sieve.19" expl="19. assertion">
<transf name="split_goal_wp">
......
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