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 int.Int
  use array.Array
  use ref.Ref
  use 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) : (m: array bool)
    requires { n > 1 }
    ensures  { 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

ObligationsAlt-Ergo 2.0.0CVC3 2.4.1CVC4 1.5Eprover 1.8-001Eprover 2.0Z3 4.6.0
VC incr------0.03---------
VC sieve------------------
split_goal_right
VC sieve.0------0.04---------
VC sieve.1------0.04---------
VC sieve.2------0.02---------
VC sieve.3------0.02---------
VC sieve.40.04---------------
VC sieve.5------0.02---------
VC sieve.6------0.02---------
VC sieve.7------------------
split_goal_right
VC sieve.7.0------0.03---------
VC sieve.7.1---------0.08------
introduce_premises
VC sieve.7.1.0------------0.04---
VC sieve.7.2------0.03---------
VC sieve.80.01---------------
VC sieve.9------0.02---------
VC sieve.10------------------
split_goal_right
VC sieve.10.0------0.03---------
VC sieve.10.1---0.02------------
remove real,tuple0,unit,map,ref,zero,one,(-),(-),(>=),abs,div1,mod1,get,even,odd,divides,prime,(!),Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Mod_bound,Div_unique,Div_bound,Mod_1,Div_1,Div_inf,Div_inf_neg,Mod_0,Div_1_left,Div_minus1_left,Mod_1_left,Mod_minus1_left,Div_mult,Mod_mult,Div_mod1,Div_bound1,Mod_bound1,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_11,Mod_11,Div_inf1,Mod_inf,Div_mult1,Mod_mult1,even_or_odd,even_not_odd,odd_not_even,even_odd,odd_even,even_even,odd_odd,even_2k,odd_2k1,even_mod2,divides_spec,divides_refl,divides_1_n,divides_0,divides_left,divides_right,divides_oppr,divides_oppl,divides_oppr_rev,divides_oppl_rev,divides_plusr,divides_minusr,divides_multl,divides_multr,divides_factorl,divides_factorr,divides_n_1,divides_antisym,divides_trans,divides_bounds,mod_divides_euclidean,divides_mod_euclidean,mod_divides_computer,divides_mod_computer,even_divides,odd_divides,not_prime_1,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,array'invariant,make_spec
VC sieve.10.1.0---------------0.02
VC sieve.10.2------0.03---------
VC sieve.110.16---------------
VC sieve.12------------------
split_goal_right
VC sieve.12.00.02---------------
VC sieve.12.10.34---------------
VC sieve.12.20.03---------------
VC sieve.12.3------0.01---------
VC sieve.12.40.01---------------
VC sieve.13------0.02---------
VC sieve.14------0.03---------
VC sieve.150.09---------------
VC sieve.16------------------
split_goal_right
VC sieve.16.00.03---------------
VC sieve.16.10.01---------------
VC sieve.16.20.04---------------
VC sieve.16.30.01---------------
VC sieve.16.4------0.02---------
VC sieve.16.50.04---------------
VC sieve.17------0.01---------
VC sieve.18------0.04---------
VC sieve.190.05---------------
VC sieve.20------------------
introduce_premises
VC sieve.20.0------------------
inline_goal
VC sieve.20.0.0------------------
split_goal_right
VC sieve.20.0.0.0------0.03---------
VC sieve.20.0.0.1------------------
introduce_premises
VC sieve.20.0.0.1.0------------------
inline_goal
VC sieve.20.0.0.1.0.00.07---------------
VC sieve.21------------------
split_goal_right
VC sieve.21.0------------0.02---
VC sieve.21.1------------------
inline_all
VC sieve.21.1.0------0.04---------
VC sieve.220.07---------------