Wiki Agenda Contact Version française

Sieve of Eratosthenes


Authors: Martin Clochard

Topics: Mathematics / Algorithms

Tools: Why3

see also the index (by topic, by tool, by reference, by year)



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

  let incr (r:ref int) : unit
    ensures { !r = old !r + 1 }
  = r := !r + 1

  let sieve (n:int) : array bool
    requires { n > 1 }
    returns { m -> length m = n /\ forall i. 0 <= i < n -> m[i] <-> prime i }
  = let t = Array.make n true in
    t[0] <- false;
    t[1] <- false;
    let i = ref 2 in
    while !i < n do
      invariant { 1 < !i <= n }
      invariant { forall j. 0 <= j < n -> t[j] <-> no_factor_lt !i j }
      variant { n - !i }
      if t[!i] then begin
        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[!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 ->
            (if l = !i then k < !r && false else false) && false) &&
          no_factor_lt (!i+1) j }
      end else assert { forall j. 0 <= j < n /\ no_factor_lt !i j ->
        (forall k l. 1 < l < !i + 1 -> j = k * l /\ k > 1 ->
          (if l = !i then (forall k0 l. 1 < l < !i /\ k0 > 1 /\ !i = k0 * l ->
              j = (k*k0) * l && false) && false
                     else false) && false) && no_factor_lt (!i+1) j };
      incr i
    done;
    assert { forall j. 0 <= j < n /\ no_factor_lt n j -> prime j };
    assert { forall j. 0 <= j < n /\ prime j ->
      forall k l. 1 < l < n /\ k > 1 -> j = k * l -> l >= j && false };
    t

end


download ZIP archive

Why3 Proof Results for Project "sieve"

Theory "sieve.Sieve": fully verified in 3.47 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)Eprover (1.8-001)Z3 (4.3.1)Z3 (4.3.2)
VC for incr0.01------------
VC for sieve---------------
split_goal_wp
  1. array creation size0.02------------
2. index in array bounds0.02------------
3. index in array bounds0.01------------
4. loop invariant init0.02------------
5. loop invariant init0.02------------
6. type invariant0.03------------
7. index in array bounds0.02------------
8. loop invariant init0.02------------
9. loop invariant init------0.05------
10. type invariant0.02------------
11. index in array bounds0.01------------
12. loop invariant preservation---------------
split_goal_wp
  1. VC for sieve------------0.02
2. VC for sieve---0.02---------
3. VC for sieve0.02------------
13. loop invariant preservation0.37------------
14. loop variant decrease0.03------------
15. assertion---------------
split_goal_wp
  1. assertion0.52------------
2. assertion0.02------------
3. assertion0.84------------
4. assertion0.01------------
5. assertion0.05------------
16. loop invariant preservation0.02------------
17. loop invariant preservation---------------
split_goal_wp
  1. loop invariant preservation0.02------------
2. loop invariant preservation0.02------------
18. loop variant decrease0.04------------
19. assertion---------------
split_goal_wp
  1. assertion0.02------------
2. assertion0.03------------
3. assertion0.02------------
4. assertion0.14------------
5. assertion0.06------------
6. assertion0.03------------
20. loop invariant preservation0.02------------
21. loop invariant preservation0.02------------
22. loop variant decrease0.03------------
23. assertion---------0.68---
24. assertion---------------
split_goal_wp
  1. assertion------0.08------
2. assertion0.04------------
25. type invariant0.03------------
26. postcondition0.02------------