## 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

Obligations | Alt-Ergo 2.0.0 | CVC3 2.4.1 | CVC4 1.5 | Eprover 1.8-001 | Eprover 2.0 | Z3 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.4 | 0.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.8 | 0.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.11 | 0.16 | --- | --- | --- | --- | --- | ||||||

VC sieve.12 | --- | --- | --- | --- | --- | --- | ||||||

split_goal_right | ||||||||||||

VC sieve.12.0 | 0.02 | --- | --- | --- | --- | --- | ||||||

VC sieve.12.1 | 0.34 | --- | --- | --- | --- | --- | ||||||

VC sieve.12.2 | 0.03 | --- | --- | --- | --- | --- | ||||||

VC sieve.12.3 | --- | --- | 0.01 | --- | --- | --- | ||||||

VC sieve.12.4 | 0.01 | --- | --- | --- | --- | --- | ||||||

VC sieve.13 | --- | --- | 0.02 | --- | --- | --- | ||||||

VC sieve.14 | --- | --- | 0.03 | --- | --- | --- | ||||||

VC sieve.15 | 0.09 | --- | --- | --- | --- | --- | ||||||

VC sieve.16 | --- | --- | --- | --- | --- | --- | ||||||

split_goal_right | ||||||||||||

VC sieve.16.0 | 0.03 | --- | --- | --- | --- | --- | ||||||

VC sieve.16.1 | 0.01 | --- | --- | --- | --- | --- | ||||||

VC sieve.16.2 | 0.04 | --- | --- | --- | --- | --- | ||||||

VC sieve.16.3 | 0.01 | --- | --- | --- | --- | --- | ||||||

VC sieve.16.4 | --- | --- | 0.02 | --- | --- | --- | ||||||

VC sieve.16.5 | 0.04 | --- | --- | --- | --- | --- | ||||||

VC sieve.17 | --- | --- | 0.01 | --- | --- | --- | ||||||

VC sieve.18 | --- | --- | 0.04 | --- | --- | --- | ||||||

VC sieve.19 | 0.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.0 | 0.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.22 | 0.07 | --- | --- | --- | --- | --- |