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 1.30Alt-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.0---0.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.2---0.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------------------