## 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.3.3 | CVC3 2.4.1 | CVC4 1.5 | Eprover 1.8-001 | Eprover 2.0 | Z3 4.12.2 | ||||||

VC for incr | --- | --- | 0.03 | --- | --- | --- | ||||||

VC for sieve | --- | --- | --- | --- | --- | --- | ||||||

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

array creation size | --- | --- | 0.04 | --- | --- | --- | ||||||

index in array bounds | --- | --- | 0.04 | --- | --- | --- | ||||||

index in array bounds | --- | --- | 0.02 | --- | --- | --- | ||||||

loop invariant init | --- | --- | 0.02 | --- | --- | --- | ||||||

loop invariant init | 0.04 | --- | --- | --- | --- | --- | ||||||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | ||||||

loop invariant init | --- | --- | 0.02 | --- | --- | --- | ||||||

loop invariant init | --- | --- | --- | --- | --- | --- | ||||||

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

loop invariant init | --- | --- | 0.03 | --- | --- | --- | ||||||

loop invariant init | --- | --- | --- | 0.08 | --- | --- | ||||||

introduce_premises | ||||||||||||

loop invariant init | --- | --- | --- | --- | 0.64 | --- | ||||||

loop invariant init | --- | --- | 0.03 | --- | --- | --- | ||||||

index in array bounds | 0.00 | --- | --- | --- | --- | --- | ||||||

loop variant decrease | --- | --- | 0.02 | --- | --- | --- | ||||||

loop invariant preservation | --- | --- | --- | --- | --- | --- | ||||||

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

VC for sieve | --- | --- | 0.03 | --- | --- | --- | ||||||

VC for sieve | --- | 0.02 | --- | --- | --- | --- | ||||||

remove real,tuple0,unit,ref,map,zero,one,(-_),(-),(>=),abs,div,mod,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,([<-])'spec,make_spec | ||||||||||||

VC for sieve | --- | --- | --- | --- | --- | 0.01 | ||||||

VC for sieve | --- | --- | 0.03 | --- | --- | --- | ||||||

loop invariant preservation | 1.65 | --- | --- | --- | --- | --- | ||||||

assertion | --- | --- | --- | --- | --- | --- | ||||||

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

assertion | 0.03 | --- | --- | --- | --- | --- | ||||||

assertion | 0.01 | --- | --- | --- | --- | --- | ||||||

assertion | 0.11 | --- | --- | --- | --- | --- | ||||||

assertion | --- | --- | 0.02 | --- | --- | --- | ||||||

assertion | 0.04 | --- | --- | --- | --- | --- | ||||||

loop variant decrease | --- | --- | 0.02 | --- | --- | --- | ||||||

loop invariant preservation | --- | --- | 0.03 | --- | --- | --- | ||||||

loop invariant preservation | 0.78 | --- | --- | --- | --- | --- | ||||||

assertion | --- | --- | --- | --- | --- | --- | ||||||

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

assertion | 0.02 | --- | --- | --- | --- | --- | ||||||

assertion | 0.01 | --- | --- | --- | --- | --- | ||||||

assertion | 0.97 | --- | --- | --- | --- | --- | ||||||

assertion | 0.03 | --- | --- | --- | --- | --- | ||||||

assertion | --- | --- | 0.01 | --- | --- | --- | ||||||

assertion | 0.01 | --- | --- | --- | --- | --- | ||||||

loop variant decrease | --- | --- | 0.01 | --- | --- | --- | ||||||

loop invariant preservation | --- | --- | 0.04 | --- | --- | --- | ||||||

loop invariant preservation | 0.05 | --- | --- | --- | --- | --- | ||||||

assertion | --- | --- | --- | --- | --- | --- | ||||||

introduce_premises | ||||||||||||

assertion | --- | --- | --- | --- | --- | --- | ||||||

inline_goal | ||||||||||||

assertion | --- | --- | --- | --- | --- | --- | ||||||

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

VC for sieve | --- | --- | 0.03 | --- | --- | --- | ||||||

VC for sieve | --- | --- | --- | --- | --- | --- | ||||||

introduce_premises | ||||||||||||

VC for sieve | --- | --- | --- | --- | --- | --- | ||||||

inline_goal | ||||||||||||

VC for sieve | 0.07 | --- | --- | --- | --- | --- | ||||||

assertion | --- | --- | --- | --- | --- | --- | ||||||

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

assertion | --- | --- | --- | --- | 0.02 | --- | ||||||

assertion | --- | --- | --- | --- | --- | --- | ||||||

inline_all | ||||||||||||

assertion | --- | --- | 0.04 | --- | --- | --- | ||||||

postcondition | 0.72 | --- | --- | --- | --- | --- |