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

Obligations | Alt-Ergo (0.99.1) | CVC3 (2.4.1) | Eprover (1.8-001) | Z3 (4.3.1) | Z3 (4.3.2) | ||

VC for incr | 0.01 | --- | --- | --- | --- | ||

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

split_goal_wp | |||||||

1. array creation size | 0.02 | --- | --- | --- | --- | ||

2. index in array bounds | 0.02 | --- | --- | --- | --- | ||

3. index in array bounds | 0.01 | --- | --- | --- | --- | ||

4. loop invariant init | 0.02 | --- | --- | --- | --- | ||

5. loop invariant init | 0.02 | --- | --- | --- | --- | ||

6. type invariant | 0.03 | --- | --- | --- | --- | ||

7. index in array bounds | 0.02 | --- | --- | --- | --- | ||

8. loop invariant init | 0.02 | --- | --- | --- | --- | ||

9. loop invariant init | --- | --- | 0.05 | --- | --- | ||

10. type invariant | 0.02 | --- | --- | --- | --- | ||

11. index in array bounds | 0.01 | --- | --- | --- | --- | ||

12. loop invariant preservation | --- | --- | --- | --- | --- | ||

split_goal_wp | |||||||

1. VC for sieve | --- | --- | --- | --- | 0.02 | ||

2. VC for sieve | --- | 0.02 | --- | --- | --- | ||

3. VC for sieve | 0.02 | --- | --- | --- | --- | ||

13. loop invariant preservation | 0.37 | --- | --- | --- | --- | ||

14. loop variant decrease | 0.03 | --- | --- | --- | --- | ||

15. assertion | --- | --- | --- | --- | --- | ||

split_goal_wp | |||||||

1. assertion | 0.52 | --- | --- | --- | --- | ||

2. assertion | 0.02 | --- | --- | --- | --- | ||

3. assertion | 0.84 | --- | --- | --- | --- | ||

4. assertion | 0.01 | --- | --- | --- | --- | ||

5. assertion | 0.05 | --- | --- | --- | --- | ||

16. loop invariant preservation | 0.02 | --- | --- | --- | --- | ||

17. loop invariant preservation | --- | --- | --- | --- | --- | ||

split_goal_wp | |||||||

1. loop invariant preservation | 0.02 | --- | --- | --- | --- | ||

2. loop invariant preservation | 0.02 | --- | --- | --- | --- | ||

18. loop variant decrease | 0.04 | --- | --- | --- | --- | ||

19. assertion | --- | --- | --- | --- | --- | ||

split_goal_wp | |||||||

1. assertion | 0.02 | --- | --- | --- | --- | ||

2. assertion | 0.03 | --- | --- | --- | --- | ||

3. assertion | 0.02 | --- | --- | --- | --- | ||

4. assertion | 0.14 | --- | --- | --- | --- | ||

5. assertion | 0.06 | --- | --- | --- | --- | ||

6. assertion | 0.03 | --- | --- | --- | --- | ||

20. loop invariant preservation | 0.02 | --- | --- | --- | --- | ||

21. loop invariant preservation | 0.02 | --- | --- | --- | --- | ||

22. loop variant decrease | 0.03 | --- | --- | --- | --- | ||

23. assertion | --- | --- | --- | 0.68 | --- | ||

24. assertion | --- | --- | --- | --- | --- | ||

split_goal_wp | |||||||

1. assertion | --- | --- | 0.08 | --- | --- | ||

2. assertion | 0.04 | --- | --- | --- | --- | ||

25. type invariant | 0.03 | --- | --- | --- | --- | ||

26. postcondition | 0.02 | --- | --- | --- | --- |