Wiki Agenda Contact Version française

Euler's Sieve

This is a variant of Eratosthenes's sieve with complexity O(N)


Authors: Josué Moreau

Topics: Mathematics / Algorithms

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


Euler's Sieve

This is a variant of Eratosthenes's sieve with complexity O(N), where N is the upper limit of the sieve. Cf https://en.wikipedia.org/wiki/Sieve_of_Eratosthenes#Euler's_sieve

Euler's Sieve makes use of a linked list of all integers, and marks composite numbers as in Eratosthenes's sieve.

In the program below, the linked list is implemented with an array (where each integer is mapped to the next one) and negative values are used to represent marked integers. In addition, the list only contains the odd integers (to save half of space).

Author: Josué Moreau (Université Paris-Saclay)

module ArithmeticResults

  use int.Int
  use number.Divisibility
  use number.Prime
  use int.EuclideanDivision

  let lemma mult_croissance_locale (n a: int)
    requires { n > 0 /\ 0 <= a }
    ensures  { n * a < n * (a + 1) } = ()

  let rec lemma mult_croissance (n a b: int)
    requires { n > 0 /\ 0 <= a < b }
    ensures  { n * a < n * b }
    variant  { b - a }
    = if a + 1 = b then ()
      else mult_croissance n (a + 1) b

  let lemma comp_mult_2 (n k: int)
    requires { n > 0 /\ k >= 2 }
    ensures  { n * k >= n * 2 } = ()

  let lemma div_croissance_locale1 (i n: int)
    requires { 0 <= i /\ n > 0 }
    ensures  { div i n <= div (i + 1) n } = ()

  let rec lemma div_croissance1 (i j n: int)
    requires { 0 <= i <= j /\ n > 0 }
    ensures  { div i n <= div j n }
    variant  { j - i }
    = if i < j then
        div_croissance1 i (j - 1) n

  let rec lemma div_croissance_locale2 (m i: int)
    requires { i > 0 /\ m >= 0 }
    ensures  { div m (i + 1) <= div m i }
    variant  { m }
    = if m > 0 then div_croissance_locale2 (m - 1) i

  let rec lemma div_croissance2 (m i j: int)
    requires { 0 < i <= j /\ m >= 0 }
    ensures  { div m i >= div m j }
    variant  { j - i }
    = if i < j then div_croissance2 m i (j - 1)

  let lemma div_mult_1 (n k max: int)
    requires { n > 0 /\ max >= n /\ n * k <= max }
    ensures  { k = div (n * k) n <= div max n } = ()

  let lemma mult_borne_sous_exp (n a b: int)
    requires { a >= 1 /\ b >= 1 /\ n >= 1 /\ a * b < n }
    ensures  { a < n /\ b < n } = ()

  let rec lemma sq_ineq (a b: int)
    requires { a >= 0 /\ b >= 0 }
    requires { a * a < b * b }
    ensures  { a < b }
    variant  { b * b - a * a }
    = if (b - 1) * (b - 1) > a * a then
        sq_ineq a (b - 1)

end

module DivisibilityResults

  use int.Int
  use int.EuclideanDivision
  use number.Divisibility
  use number.Prime

  let lemma divides_div (n m k: int)
    requires { 2 <= n /\ 2 <= m /\ 2 <= k < n /\ divides n m /\ not divides k m }
    ensures  { not divides k (div m n) } = ()

  let lemma divides_inf (n m: int)
    requires { 2 <= n /\ 2 <= m /\ divides n m /\
               forall k. 2 <= k < n -> not divides k m }
    ensures  { forall k. 2 <= k < n -> not divides k (div m n) } = ()

  let lemma not_prime_divider_limits (n: int)
    requires { not prime n /\ 2 <= n }
    ensures  { exists i. 2 <= i /\ i * i <= n /\ divides i n } = ()

  let lemma no_prod_impl_no_divider (n: int)
    requires { n >= 0 }
    ensures  { forall i.
                 2 <= i < n * n ->
                 not (exists k l. 2 <= k < n /\ 2 <= l < i /\ k * l = i ) ->
                 not (exists k. 2 <= k < n /\ k <> i /\ divides k i) } = ()

  use ArithmeticResults

  let lemma not_prime_impl_divisor_under_sqrt (n: int)
    requires { n >= 2 }
    ensures  { forall i.
                 2 <= i < n * n ->
                 not prime i ->
                 exists j. 2 <= j < i /\ ((j < n)
                           by j * j < n * n /\ j >= 0) /\ divides j i } = ()

end

module EulerSieveSpec

  use int.Int
  use number.Divisibility
  use number.Prime
  use seq.Seq
  use int.EuclideanDivision

  use ArithmeticResults
  use DivisibilityResults

(*                                                                             *)
(*         INVARIANTS SUR LES RELATIONS ENTRE STRUCTURES DE DONNEES            *)
(*                                                                             *)

  (* Borne sur le suivant de chaque élément de la liste chaînée *)
  predicate inv_nexts (nexts: seq int) (n: int) =
    forall i. 0 <= i < n ->
              i < nexts[i] <= n

  (* Tous les éléments éliminés de la liste chaînée sont marqués *)
  predicate all_eliminated_marked (marked: seq bool)
                                  (nexts: seq int) =
    marked.length = nexts.length /\
    forall i. 0 <= i < marked.length ->
              forall j. i < j < nexts[i] ->
                        marked[j]

  (* Tous les éléments éliminés, à partir d'un certain indice, sont marqués *)
  predicate all_eliminated_marked_partial (marked: seq bool)
                                          (nexts: seq int)
                                          (min: int) =
    marked.length = nexts.length /\
    forall i. min <= i < marked.length ->
              forall j. i < j < nexts[i] ->
                        marked[j]

  (* L'élément suivant d'un élément non marqué inférieur à max / n est
     non marqué lorsqu'il est lui-même inférieur à max / n *)
  predicate not_marked_impl_next_not_marked (marked_old: seq bool)
                                            (nexts: seq int)
                                            (n: int) =
    marked_old.length = nexts.length /\
    marked_old.length >= 2 /\
    n >= 2 /\
    forall i. 2 <= i <= div (marked_old.length - 1) n ->
              nexts[i] <= div (marked_old.length - 1) n ->
              not marked_old[i] ->
              not marked_old[nexts[i]]

  (* Les deux tableaux marked sont identiques *)
  predicate is_copy (marked: seq bool)
                    (marked_old: seq bool) =
    marked.length = marked_old.length /\
    forall i. 0 <= i < marked.length ->
              not marked[i] ->
              not marked_old[i]

  (* L'élément suivant d'un élément non marqué inférieur à p <= max / n est
     non marqué lorsqu'il est inférieur à max / n *)
  predicate not_marked_impl_next_not_marked_partial (marked: seq bool)
                                                    (nexts: seq int)
                                                    (n: int)
                                                    (p: int) =
    marked.length = nexts.length /\
    marked.length >= 2 /\
    n >= 2 /\
    p <= div (marked.length - 1) n /\
    forall i. 2 <= i < p ->
              nexts[i] <= div (marked.length - 1) n ->
              not marked[i] ->
              not marked[nexts[i]]

(*                                                                             *)
(*                   PROPRIETES LIEES AUX NOMBRES PREMIERS                     *)
(*                                                                             *)

  (* Tous les nombres jusqu'à n sont non marqués si et seulement si ils sont
     premiers *)
  predicate all_primes (marked: seq bool) (n: int) =
    forall i. 0 <= i < n -> not marked[i] <-> prime i

  (* Tous les multiples de i sont marqués *)
  predicate all_multiples_marked (marked: seq bool) (i max: int) =
    2 <= i < marked.length /\
    forall k. 2 <= k < max ->
              i * k < marked.length ->
              marked[i * k]

  (* Tous les multiples des 2 <= i < n sont marqués *)
  predicate previously_marked_multiples (marked: seq bool) (n: int) =
    forall i. 2 <= i < n ->
              all_multiples_marked marked i marked.length

  (* Les multiples des 2 <= i < n sont les uniques nombres marqués *)
  predicate only_multiples_marked (marked: seq bool) (n: int) =
    forall k. 2 <= k < marked.length ->
              marked[k] ->
              exists i j. 2 <= i < n /\ 2 <= j < marked.length /\ i * j = k

  (* Les multiples de n avec les éléments non marqués précédement sont
     marqués *)
  predicate prime_multiples_marked (marked_old: seq bool)
                                   (marked: seq bool)
                                   (n max: int) =
    marked_old.length = marked.length /\
    n < max <= marked.length /\
    forall i. n <= i < max ->
              not marked_old[i] ->
              n * i < marked_old.length ->
              marked[n * i]

  (* Invariants de base de remove_products *)
  predicate inv_remove_products (nexts: seq int)
                                (marked: seq bool)
                                (n: int) =
    nexts.length = marked.length /\
    not marked[2] /\
    all_primes marked n /\
    prime n /\
    not marked[n] /\
    inv_nexts nexts nexts.length

(*                                                                             *)
(*             QUELQUES LEMMES DE CONSERVATION DES STRUCTURES                  *)
(*                                                                             *)

  let lemma conservation_all_eliminated_marked_on_marked_change
      (marked: seq bool)
      (nexts: seq int)
      (i: int)
    requires { marked.length = nexts.length }
    requires { inv_nexts nexts nexts.length }
    requires { all_eliminated_marked marked nexts }
    requires { 0 <= i < marked.length }
    ensures  { all_eliminated_marked marked[i <- true] nexts } = ()

  let lemma conservation_all_eliminated_marked_on_nexts_change
      (marked: seq bool)
      (nexts: seq int)
      (i v: int)
    requires { marked.length = nexts.length }
    requires { all_eliminated_marked marked nexts }
    requires { inv_nexts nexts marked.length }
    requires { 0 <= i < marked.length }
    requires { i < v <= marked.length }
    requires { forall j. i < j < v -> marked[j] }
    ensures  { all_eliminated_marked marked nexts[i <- v] } = ()

(*                                                                             *)
(*                         QUELQUES PREDICATS UTILES                           *)
(*                                                                             *)

  predicate ordered (a: seq int) (n: int) =
    forall i j. 0 <= i < j < n -> a[i] < a[j]

  predicate all_inf_or_eq (a: seq int) (n k: int) =
    forall i. 0 <= i < n -> a[i] <= k

end

module EulerSieve

  use int.Int
  use number.Divisibility
  use number.Prime
  use seq.Seq
  use int.EuclideanDivision

  use ArithmeticResults
  use DivisibilityResults

  use EulerSieveSpec

(*                                                                             *)
(*                   PROPRIETES LIEES AUX NOMBRES PREMIERS                     *)
(*                                                                             *)

  (* Si tous les multiples des nombres i < n sont marqués,
     alors les mutliples de ces multiples sont marqués *)
  let lemma multiples_of_marked_are_marked (marked: seq bool) (n: int)
    requires { 2 <= n <= marked.length }
    requires { previously_marked_multiples marked n }
    ensures  { forall k i.
                2 <= k < n ->
                2 <= i < marked.length ->
                k * i < marked.length ->
                forall j.
                  1 <= j < marked.length ->
                  k * i * j < marked.length ->
                  (marked[k * i * j]
                   by 1 <= i * j < marked.length
                   by k >= 2 /\ i >= 2 /\ j >= 1 /\ k * (i * j) < marked.length) }
    = ()

  (* Lemme essentiel : si tous les multiples des nombres i < n sont marqués
                       et qu'on a marqué tous les produits de n avec les nombres
                       non marqués
                       alors tous les multiples de n sont marqués *)
  let lemma prev_and_new_impl_all_multiples_marked
      (marked_old marked: seq bool)
      (n max: int)
    requires { 2 <= n < marked.length /\ 2 <= max < marked.length /\
               marked_old.length = marked.length }
    requires { is_copy marked marked_old }
    requires { previously_marked_multiples marked_old n }
    requires { previously_marked_multiples marked n }
    requires { only_multiples_marked marked_old n }
    requires { prime_multiples_marked marked_old marked n marked.length }
    ensures  { all_multiples_marked marked n marked.length } =
    assert { forall i. 2 <= i < n /\ 2 <= i < marked.length ->
                       not marked_old[i] ->
                       i * n < marked.length ->
                       marked[i * n] };
    assert { forall k. 2 <= k < marked_old.length ->
                       marked_old[k] ->
                       n * k < marked_old.length ->
                       exists i j. 2 <= i < n /\ 2 <= j < marked_old.length /\
                                   i * j = k /\ marked_old[i * j] };
    multiples_of_marked_are_marked marked_old n;
    multiples_of_marked_are_marked marked n;
    assert { marked.length = marked_old.length };
    assert { forall k. 2 <= k < marked_old.length ->
                       marked_old[k] ->
                       n * k < marked_old.length ->
                       marked[k * n]
             by forall k. 2 <= k < marked_old.length ->
                       marked_old[k] ->
                       n * k < marked_old.length ->
                       marked_old[k * n] };
    assert { prime_multiples_marked marked_old marked n marked.length };
    assert { (forall k. 2 <= k < marked.length ->
                       not marked_old[k] -> n * k < marked.length ->
                       marked[n * k]) }

(*                                                                             *)
(*             LEMMES DE CONSERVATION LIES AUX NOMBRES PREMIERS                *)
(*                                                                             *)

  let lemma conservation_only_multiples_marked (marked: seq bool) (n i j: int)
    requires { 2 <= i < n /\ 2 <= j < marked.length /\ i * j < marked.length }
    requires { only_multiples_marked marked n }
    ensures  { only_multiples_marked marked[(i * j) <- true] n } =
    assert { forall k. 0 <= k < marked.length ->
                       k <> i * j ->
                       marked[(i * j) <- true][k] = marked[k] };
    assert { forall k.
               2 <= k < marked.length ->
               k <> i * j ->
               marked[(i * j) <- true][k] ->
               exists x y. 2 <= x < n /\ 2 <= y < marked.length /\ k = x * y };
    assert { marked[i * j] -> 2 <= i < n -> 2 <= j < marked.length ->
             exists x y. 2 <= x < n /\ 2 <= y < marked.length /\ x * y = i * j }

  let lemma conservation_previously_marked_multiples (marked: seq bool)
                                                     (nexts: seq int)
                                                     (n: int)
    requires { 2 <= n < marked.length /\ marked.length = nexts.length /\
               nexts[n] <= marked.length }
    requires { previously_marked_multiples marked n }
    requires { only_multiples_marked marked (n + 1) }
    requires { all_eliminated_marked marked nexts }
    requires { not_marked_impl_next_not_marked marked nexts nexts[n] }
    requires { all_multiples_marked marked n marked.length }
    ensures  { previously_marked_multiples marked nexts[n] } =
    assert { previously_marked_multiples marked (n + 1) };
    assert { forall i. n < i < nexts[n] -> marked[i] };
    assert { forall i. n < i < nexts[n] ->
              ((exists k l. 2 <= k <= n /\ 2 <= l < marked.length /\ k * l = i)
               by marked[i]) };
    multiples_of_marked_are_marked marked (n + 1);
    assert { forall i j.
              n < i < nexts[n] ->
              2 <= j < marked.length ->
              i * j < marked.length ->
              (marked[i * j]
               by (exists k l. 2 <= k <= n /\ 2 <= l < marked.length /\ k * l = i)) };
    assert { forall i.
              n < i < nexts[n] ->
              all_multiples_marked marked i marked.length }

  lemma conservation_previously_marked_multiples_on_marked_change:
    forall marked n.
      previously_marked_multiples marked n ->
      forall i. 0 <= i < marked.length ->
                previously_marked_multiples marked[i <- true] n

(*                                                                             *)
(*                      INVARIANTS SIMPLES DE FONCTIONS                        *)
(*                                                                             *)

  let lemma conservation_not_marked_impl_next_not_marked
      (marked: seq bool)
      (nexts: seq int)
      (max n p: int)
    requires { not_marked_impl_next_not_marked marked nexts n /\
                 nexts[n] > n > 0 /\
                 div max nexts[n] <= div max n
                 by forall i. p < i < nexts[p] -> marked[i] /\
                    not_marked_impl_next_not_marked_partial marked nexts n p }
    ensures  { not_marked_impl_next_not_marked marked nexts nexts[n] } = ()

  let lemma unchanged_other_elements (s1: seq 'a) (s2: seq 'a) (i: int) (v: 'a)
    requires { 0 <= i < length s1 /\ length s1 = length s2 }
    requires { s1 = s2[i <- v] }
    ensures  { forall j. 0 <= j < length s1 -> i <> j -> s1[j] = s2[j] } = ()

(*                                                                             *)
(*              DEFINITION DE LA STRUCTURE DE DONNEE ABSTRAITE                 *)
(*                                                                             *)

  use mach.int.Int63

  type t = private {
    mutable ghost nexts: seq int;
    mutable ghost marked: seq bool;
    max: int63;
  }
    invariant { max_int > max >= 3 }
    invariant { nexts.length = marked.length = max + 1 }
    invariant { inv_nexts nexts nexts.length }
    invariant { all_eliminated_marked marked nexts }
    invariant { forall i. 3 <= i <= max -> mod i 2 = 0 -> marked[i] }
    invariant { forall i. 3 <= i < max - 1 ->
                          mod i 2 = 1 ->
                          mod (Seq.get nexts i) 2 = 1 \/ Seq.get nexts i = max + 1 }
    invariant { Seq.get nexts max = max + 1 /\
                (mod (max - 1) 2 = 0 -> Seq.get nexts (max - 1) = max) /\
                (mod (max - 1) 2 = 1 -> Seq.get nexts (max - 1) = max + 1) }

    by { nexts = Seq.create 4 (fun i -> i + 1);
         marked = Seq.create 4 (fun i -> i < 2);
         max = 3 }

  val create (max: int63) : t
    requires { max_int > max >= 3 }
    ensures  { result.max = max }
    ensures  { Seq.get result.marked 0 = Seq.get result.marked 1 = true /\
               not Seq.get result.marked 2 }
    ensures  { forall i. 3 <= i <= max ->
                         mod i 2 = 0 <-> Seq.get result.marked i }
    ensures  { forall i. 3 <= i < max - 1 ->
                         mod i 2 = 0 -> Seq.get result.nexts i = i + 1 }
    ensures  { forall i. 3 <= i < max - 1 ->
                         mod i 2 = 1 -> Seq.get result.nexts i = i + 2 }
    ensures  { forall i. 0 <= i <= max ->
                         Seq.get result.marked i -> i < 2 \/ divides 2 i }

  val set_next (t: t) (i v: int63) : unit
    requires { 0 <= i <= t.max /\ i < v <= t.max + 1 }
    requires { mod i 2 = 1 }
    requires { forall j. i < j < v -> Seq.get t.marked j }
    requires { not Seq.get t.marked i }
    requires { mod v 2 = 1 \/ v = t.max + 1 }
    writes   { t.nexts }
    ensures  { t.nexts = (old t.nexts)[i <- v] }

  val get_next (t: t) (i: int63) : int63
    requires { 3 <= i <= t.max }
    requires { mod i 2 = 1 }
    ensures  { 3 <= result <= t.max + 1 }
    ensures  { result = t.nexts[i] }
    ensures  { mod result 2 = 1 \/ result = t.max + 1 }

  val set_mark (t: t) (i: int63) : unit
    requires { 0 <= i <= t.max }
    requires { mod i 2 = 1 }
    writes   { t.marked }
    ensures  { t.marked = (old t.marked)[i <- true] }

  val get_mark (t: t) (i: int63) : bool
    requires { 0 <= i <= t.max }
    requires { mod i 2 = 1 }
    ensures { result = t.marked[i] }

  val get_max (t: t) : int63
    ensures { result = t.max /\ result >= 2 }

(*                                                                             *)
(*     PREUVE DE REMOVE_PRODUCTS DANS LA STRUCTURE DE DONNEE ABSTRAITE         *)
(*                                                                             *)

  let remove_products (t: t) (n: int63) : unit
    requires { 3 <= n <= t.max /\ n * n <= t.max }
    requires { inv_remove_products t.nexts t.marked n }
    requires { previously_marked_multiples t.marked n }
    requires { only_multiples_marked t.marked n }
    requires { not_marked_impl_next_not_marked t.marked t.nexts n }
    ensures  { inv_remove_products t.nexts t.marked n }
    ensures  { not_marked_impl_next_not_marked t.marked t.nexts t.nexts[n] }
    ensures  { previously_marked_multiples t.marked t.nexts[n] }
    ensures  { only_multiples_marked t.marked t.nexts[n] }
    = let d = get_max t / n in
      let ghost max = t.max in
      let ghost marked_old = t.marked in
      let rec loop (p: int63) (ghost x: int) =
        requires { n <= p <= max /\ 3 <= n <= max /\ mod p 2 = 1 /\
                   p <= x < t.nexts[p] /\ t.nexts[x] = t.nexts[p] /\
                   t.marked[n * n] }
        requires { inv_remove_products t.nexts t.marked n }
        requires { previously_marked_multiples t.marked n }
        requires { not t.marked[p] }
        requires { is_copy t.marked marked_old }
        requires { all_eliminated_marked_partial marked_old t.nexts x }
        requires { not_marked_impl_next_not_marked marked_old t.nexts n }
        requires { prime_multiples_marked marked_old t.marked n t.nexts[x] }
        requires { not_marked_impl_next_not_marked_partial t.marked t.nexts n p }
        requires { only_multiples_marked t.marked (n + 1) }
        ensures  { inv_remove_products t.nexts t.marked n }
        ensures  { not_marked_impl_next_not_marked t.marked t.nexts t.nexts[n] }
        ensures  { is_copy t.marked marked_old }
        ensures  { previously_marked_multiples t.marked n }
        ensures  { prime_multiples_marked marked_old t.marked n t.marked.length }
        ensures  { only_multiples_marked t.marked (n + 1) }
        variant  { max - t.nexts[p] }
        let next = get_next t p in
        if 0 <= next <= get_max t then
          if next <= d then begin
            assert { n * next <= max by n * next <= n * d by next <= d };
            ghost (conservation_only_multiples_marked t.marked (to_int n + 1)
                              (to_int n) t.nexts[to_int p]);
            let ghost marked_copy = t.marked in
            set_mark t (n * next);
            unchanged_other_elements t.marked marked_copy
                                     (to_int n * to_int next) true;
            assert { p < 2 * p < 2 * t.nexts[p] <= n * t.nexts[p] = n * next };
            assert { not t.marked[p] by n * next > p /\ p <= length t.marked };
            assert { not marked_old[t.nexts[p]] by 2 <= p < next <= div max n };
            assert { prime_multiples_marked marked_old t.marked n t.nexts[next]
                     by prime_multiples_marked marked_old t.marked n t.nexts[x] };
            assert { forall i. 0 <= i < p -> t.nexts[i] <= p
                     by forall i. 0 <= i < p ->
                                  forall j. i < j < t.nexts[i] -> t.marked[j] };
            if get_mark t next then begin
              assert { t.nexts[p] <> t.marked.length };
              let ghost nexts_copy = t.nexts in
              set_next t p (get_next t next);
              unchanged_other_elements t.nexts nexts_copy (to_int p)
                                       nexts_copy[to_int next];
              assert { all_eliminated_marked_partial marked_old t.nexts next
                       by p <= x < next /\
                          forall j. next <= j < length t.nexts ->
                                    t.nexts[j] = nexts_copy[j] };
              loop p (to_int next)
            end else begin
              assert { forall i. p < i < t.nexts[p] -> t.marked[i] };
              loop next (to_int next)
            end
          end else begin
            assert { n * next > max
                     by n * (div max n + 1) > max >= n * div max n /\
                        n * next >= n * (d + 1) by next >= d + 1 };
            ghost (conservation_not_marked_impl_next_not_marked t.marked t.nexts
                                  (to_int max) (to_int n) (to_int p))
        end else
          ghost (conservation_not_marked_impl_next_not_marked t.marked t.nexts
                                  (to_int max) (to_int n) (to_int p)) in
        ghost (conservation_only_multiples_marked t.marked (to_int n + 1)
                                                  (to_int n) (to_int n));
        let ghost marked_copy = t.marked in
        set_mark t (n * n);
        unchanged_other_elements t.marked marked_copy (to_int n * to_int n) true;
        assert { forall i. 0 <= i < n -> t.nexts[i] <> n * n
                 by forall i. 0 <= i < n -> t.nexts[i] <= n < n * n
                 by not t.marked[n] /\
                    forall i. 0 <= i < n ->
                              forall j. i < j < t.nexts[i] -> t.marked[j] };
        loop n (to_int n);
        ghost (prev_and_new_impl_all_multiples_marked marked_old t.marked
                                                      (to_int n) (to_int max));
        ghost (conservation_previously_marked_multiples t.marked t.nexts
                                                        (to_int n))

(*                                                                             *)
(*           QUELQUES LEMMES NECESSAIRES A LA SUITE DE LA PREUVE               *)
(*                                                                             *)

  let lemma previously_marked_multiples_impl_prime (marked: seq bool) (n: int)
    requires { 2 <= n < marked.length /\ not marked[n] }
    requires { previously_marked_multiples marked n }
    ensures  { prime n } =
    assert { forall k.
               2 <= k < n -> not divides k n
             by forall k.
                  2 <= k < n ->
                  not (exists i. 2 <= i < marked.length /\ n = k * i) }

  let lemma only_multiples_marked_impl_not_marked (marked: seq bool)
                                                 (nexts: seq int)
                                                 (n: int)
    requires { 2 <= n < marked.length }
    requires { only_multiples_marked marked nexts[n] }
    requires { prime n }
    ensures  { not marked[n] } =
    assert { forall i j. 2 <= i < n -> 2 <= j < marked.length -> i * j <> n }

end

module EulerSieveImpl

  use int.Int
  use seq.Seq
  use mach.int.Int63
  use mach.array.ArrayInt63

  use int.Abs
  use int.EuclideanDivision
  use number.Divisibility
  use number.Prime

  use DivisibilityResults
  use EulerSieveSpec

(*                                                                             *)
(*              LEMMES DE CONSERVATION LIES A L'IMPLEMENTATION                 *)
(*                                                                             *)

  let lemma conservation_inv_arr_on_mark (arr: seq int) (i: int)
    requires { forall j k. 0 <= j < length arr ->
                           j < k < div (abs arr[j]) 2 -> arr[k] < 0 }
    requires { forall i. 0 <= i < length arr ->
                         i < div (abs arr[i]) 2 <= length arr }
    requires { 0 <= i < length arr }
    requires { arr[i] >= 0 }
    ensures  { forall j k. 0 <= j < length arr ->
                           j < k < div (abs arr[i <- - arr[i]][j]) 2 ->
                           arr[i <- - arr[i]][k] < 0 } =
    assert { forall j. 0 <= j < length arr ->
                       arr[j] < i -> arr[j] = arr[i <- - arr[i]][j] };
    assert { forall j. 0 <= j < length arr ->
                       arr[i] < j -> arr[j] = arr[i <- - arr[i]][j] }

  let lemma conservation_inv_arr_on_jump (arr: seq int) (min i: int)
    requires { min >= 0 }
    requires { forall j k. min <= j < length arr ->
                           j < k < div (abs arr[j]) 2 -> arr[k] < 0 }
    requires { forall i. min <= i < length arr ->
                         i < div (abs arr[i]) 2 <= length arr }
    requires { min <= i < length arr }
    requires { 0 <= div arr[i] 2 < length arr }
    requires { arr[div arr[i] 2] < 0 }
    ensures  { forall j k. min <= j < length arr ->
                           j < k < div (abs arr[i <- - arr[div arr[i] 2]][j]) 2 ->
                           arr[i <- - arr[div arr[i] 2]][k] < 0 } =
    let ghost next = div (Seq.get arr i) 2 in
    let ghost arr1 = arr[i <- - Seq.get arr next] in
    assert { forall j. min <= j < i -> arr[j] = arr1[j] };
    assert { forall j. i < j < length arr -> arr[j] = arr1[j] }

(*                                                                             *)
(*         DEFINITION DE L'IMPLEMENTATION DE LA STRUCTURE DE DONNEE            *)
(*                                                                             *)

  type t = {
    mutable ghost nexts: seq int;
    mutable ghost marked: seq bool;
    arr: array63;
    max: int63;
    max_arr: int63
  }
    invariant { max_int > max >= 3 }
    invariant { Seq.length nexts = Seq.length marked = max + 1 }
    invariant { div (max - 1) 2 = max_arr }
    invariant { length arr = max_arr + 1 }
    invariant { inv_nexts nexts (Seq.length nexts) }
    invariant { all_eliminated_marked marked nexts }
    invariant { forall i. 3 <= i <= max -> mod i 2 = 0 -> Seq.get marked i }
    invariant { forall i. 3 <= i < max - 1 ->
                          mod i 2 = 1 ->
                          mod (Seq.get nexts i) 2 = 1 \/ Seq.get nexts i = max + 1 }
    invariant { Seq.get nexts max = max + 1 /\
                (mod (max - 1) 2 = 0 -> Seq.get nexts (max - 1) = max) /\
                (mod (max - 1) 2 = 1 -> Seq.get nexts (max - 1) = max + 1) }
    (* glueing invariant *)
    invariant { forall i. 0 <= i <= max_arr -> -(max + 1) <= arr[i] <= max + 1 }
    invariant { forall i. 0 <= i <= max_arr ->
                          Seq.get marked (2 * i + 1) <-> arr[i] < 0 }
    invariant { forall i. 0 <= i <= max_arr ->
                          not Seq.get marked (2 * i + 1) ->
                          arr[i] = Seq.get nexts (2 * i + 1) }
    invariant { forall i. 0 <= i <= max_arr ->
                          Seq.get marked (2 * i + 1) ->
                          arr[i] = - Seq.get nexts (2 * i + 1) }
    invariant { forall i. 0 <= i <= max_arr ->
                          i < div (abs arr[i]) 2 <= max_arr + 1 /\
                          abs arr[i] <= max + 1 }
    invariant { forall i j. 0 <= i <= max_arr ->
                            i < j < div (abs arr[i]) 2 -> arr[j] < 0 }
    by { nexts = Seq.create 4 (fun i -> i + 1);
         marked = Seq.create 4 (fun i -> i < 2);
         arr = ArrayInt63.set (ArrayInt63.make 2 (-2)) 1 4;
         max = 3; max_arr = 1 }

  let create (max: int63) : t
    requires { max_int > max >= 3 }
    ensures  { result.max = max }
    ensures  { Seq.get result.marked 0 = Seq.get result.marked 1 = true /\
               not Seq.get result.marked 2 }
    ensures  { forall i. 1 <= i <= div (max - 1) 2 ->
                         not Seq.get result.marked (2 * i + 1) }
    ensures  { forall i. 2 <= i <= div (max + 1) 2 ->
                         2 * i <= max ->
                         Seq.get result.marked (2 * i) }
    ensures  { forall i. 1 <= i <= div (max - 1) 2 ->
                         2 * i + 1 < max - 1 ->
                         Seq.get result.nexts (2 * i + 1) = 2 * i + 3 }
    ensures  { forall i. 2 <= i <= div (max - 1) 2 ->
                         2 * i < max - 1 ->
                         Seq.get result.nexts (2 * i) = 2 * i + 1 }
    ensures  { forall i. 0 <= i <= max ->
                         Seq.get result.marked i -> i < 2 \/ divides 2 i }
  = let ghost len = pure { max + 1 } in
    let len_arr = (max - 1) / 2 + 1 in
    let ghost nexts = Seq.create len (pure { fun (i: int) ->
          if i = max then max + 1
          else if i = max - 1 then if mod i 2 = 0 then max else max + 1
          else if i < 3 || mod i 2 = 0 then i + 1
          else i + 2}) in
    let ghost marked = Seq.create len (fun i ->
          i = 0 || i = 1 || (i > 2 && mod i 2 = 0)) in
    let ghost f = pure { fun i -> if i = len_arr - 1 then max + 1
          else if i = 0 then -2
          else 2 * i + 3 } in
    let arr = ArrayInt63.make len_arr (-2) in
    for i = 1 to len_arr - 1 do
      invariant { forall j. 0 <= j < i -> arr[j] = f j }
      arr[i] <- if i = len_arr - 1 then max + 1 else 2 * i + 3
    done;
    { nexts = nexts;
      marked = marked;
      arr = arr;
      max = max;
      max_arr = (max - 1) / 2 }

  let set_next (t: t) (i v: int63) : unit
    requires { 0 <= i <= t.max /\ i < v <= t.max + 1 }
    requires { mod i 2 = 1 }
    requires { forall j. i < j < v -> Seq.get t.marked j }
    requires { not Seq.get t.marked i }
    requires { mod v 2 = 1 \/ v = t.max + 1 }
    writes   { t.nexts, t.arr }
    ensures  { t.nexts = Seq.set (old t.nexts) i v }
  = ghost ( conservation_all_eliminated_marked_on_nexts_change
                      t.marked t.nexts (to_int i) (to_int v) );
    t.arr[i / 2] <- v;
    ghost (t.nexts <- Seq.set t.nexts (to_int i) (to_int v))

  let get_next (t: t) (i: int63) : int63
    requires { 3 <= i <= t.max }
    requires { mod i 2 = 1 }
    ensures  { 3 <= result <= t.max + 1 }
    ensures  { result = Seq.get t.nexts i }
    ensures  { mod result 2 = 1 \/ result = t.max + 1 }
  = let x = i / 2 in
    if t.arr[x] < 0 then - t.arr[x] else t.arr[x]

  let set_mark (t: t) (i: int63) : unit
    requires { 0 <= i <= t.max }
    requires { mod i 2 = 1 }
    writes   { t.marked, t.arr }
    ensures  { t.marked = Seq.set (old t.marked) i true }
  = let x = i / 2 in
    ghost ( conservation_all_eliminated_marked_on_marked_change
                              t.marked t.nexts (to_int i));
    if t.arr[x] >= 0 then begin
      ghost ( conservation_inv_arr_on_mark t.arr.elts (to_int x) );
      t.arr[x] <- - t.arr[x]
    end;
    ghost (t.marked <- Seq.set t.marked (to_int i) true)

  let get_mark (t: t) (i: int63) : bool
    requires { 0 <= i <= t.max }
    requires { mod i 2 = 1 }
    ensures  { result = Seq.get t.marked i }
  = t.arr[i / 2] < 0

  let get_max (t: t) : int63
    ensures { result = t.max /\ result >= 2 }
  = t.max

  clone EulerSieve with type t = t,
    val create = create,
    val set_next = set_next, val get_next = get_next,
    val set_mark = set_mark, val get_mark = get_mark,
    val get_max = get_max

  predicate inv_count (arr: seq int) (min: int) =
    forall i. min <= i < arr.length ->
              (i < div (abs arr[i]) 2 <= arr.length /\
               - max_int <= arr[i] <= max_int /\
               (forall j. i < j < div (abs arr[i]) 2 -> arr[j] < 0) /\
               (forall j. 2 * i + 1 < j < abs arr[i] -> not prime j))

(*                                                                             *)
(*                         PREUVE DU CRIBLE D'EULER                            *)
(*                                                                             *)

  let euler_sieve (max: int63) : array63
    requires { max_int > max >= 3 }
    ensures  { forall i j. 0 <= i < j < result.length -> result[i] < result[j] }
    ensures  { forall i. 0 <= i < result.length -> 2 <= result[i] <= max }
    ensures  { forall i. 0 <= i < result.length -> prime result[i] }
    ensures  { forall i. 2 <= i <= max -> prime i ->
                         exists j. 0 <= j < result.length /\ result[j] = i }
  = [@vc:do_not_keep_trace] (* traceability info breaks the proof with Vampire on sub goal 13.2 *)
    let t = create max in
    let rec loop (n: int63) =
      requires { 3 <= n <= max }
      requires { n * n <= max }
      requires { previously_marked_multiples t.marked n }
      requires { only_multiples_marked t.marked n }
      requires { not_marked_impl_next_not_marked t.marked t.nexts n }
      requires { inv_remove_products t.nexts t.marked n }
      ensures { forall i. 0 <= i < Seq.length t.marked ->
                          not Seq.get t.marked i <-> prime i }
      variant { max + 1 - n }
        remove_products t n;
        let nn = get_next t n in
        if nn <= max / nn then begin
          assert { nn * nn <= max };
          ghost (previously_marked_multiples_impl_prime t.marked (to_int nn));
          assert { (forall i. n < i < nn -> not prime i)
                   by (forall i.
                      n < i < nn ->
                      (exists j k.
                         2 <= j < nn /\
                         2 <= k < Seq.length t.marked /\
                         j * k = i)
                         by Seq.get t.marked i) };
          loop (nn)
        end else begin
          ghost (not_prime_impl_divisor_under_sqrt (to_int nn));
          assert { forall i.
                     2 <= i < Seq.length t.marked ->
                     not Seq.get t.marked i ->
                     not (exists k l. 2 <= k < nn /\ 2 <= l < i /\
                                      k * l = i) };
          ghost (no_prod_impl_no_divider (to_int nn));
          assert { Seq.length t.marked <= nn * nn
                   by nn * nn > max
                   by nn * (div max nn + 1) > max >= nn * div max nn
                      /\ nn * nn >= nn * (div max nn + 1)
                   by nn >= div max nn + 1 };
          assert { forall i. 2 <= i < Seq.length t.marked ->
                             not Seq.get t.marked i ->
                             prime i
                   by forall i.
                        2 <= i < Seq.length t.marked ->
                        not Seq.get t.marked i ->
                        (not (exists k. 2 <= k < nn /\ k <> i /\
                                        divides k i)
                         by forall k.
                              2 <= k ->
                              k <> i ->
                              (divides k i <-> exists l. 2 <= l < i /\ k * l = i)
                              by divides k i -> 2 <= div i k < i) }
        end in
    if max >= 9 then loop 3;
    assert { forall i. 1 <= i <= t.max_arr -> t.arr[i] >= 0 <-> prime (2 * i + 1) };
    assert { forall p i. 1 <= p <= t.max_arr ->
                         2 * p + 1 < i < abs t.arr[p] -> not prime i
             by mod i 2 = 0 -> (Seq.get t.marked i
             by Seq.get t.nexts (2 * i + 1) = t.arr[i]) };
    assert { forall j. 1 <= j <= t.max_arr -> t.arr[0 <- 2][j] = t.arr[j] };
    let ref cnt = 1:int63 in
    let ref p = 1 in
    t.arr[0] <- 2;
    while 2 * p + 1 <= max do
      invariant { 1 <= p <= t.max_arr + 1 }
      invariant { 1 <= cnt <= p }
      invariant { 2 * p + 1 <= max -> t.arr[p] >= 0 }
      invariant { 2 * p + 1 <= max -> prime (2 * p + 1) }
      invariant { inv_count t.arr cnt }
      invariant { ordered t.arr cnt }
      invariant { all_inf_or_eq t.arr cnt (2 * p) }
      invariant { forall i. cnt <= i <= t.max_arr ->
                            t.arr[i] >= 0 <-> prime (2 * i + 1) }
      invariant { forall i. 0 <= i < cnt -> prime t.arr[i] }
      invariant { forall i. 2 <= i < 2 * p + 1 -> prime i ->
                            exists j. 0 <= j < cnt /\ t.arr[j] = i }
      variant { t.max_arr + 1 - p , max + 1 - t.arr[p] }
      let next = t.arr[p] / 2 in
      if next <= t.max_arr then begin
        assert { 1 <= p <= t.max_arr /\ t.arr[p] >= 0 /\ prime (2 * p + 1) };
        if t.arr[next] < 0 then begin
          label BeforeAssign in
          t.arr[p] <- - t.arr[next];
          unchanged_other_elements t.arr.elts (pure { t.arr.elts at BeforeAssign })
                                   (to_int p) (- to_int t.arr[next]);
          assert { forall i. p < i < div t.arr[p] 2 -> t.arr[i] < 0 };
          assert { t.arr[p] = abs (t.arr at BeforeAssign)[next]
                            > (t.arr at BeforeAssign)[p] > p };
          conservation_inv_arr_on_jump (pure { t.arr.elts at BeforeAssign })
                                       (to_int cnt) (to_int p);
          assert { cnt <= next < length t.arr };
          assert { (forall j. 2 * p + 1 < j < (t.arr at BeforeAssign)[p] ->
                              not prime j) /\
                   (forall j. 2 * next + 1 < j < abs (t.arr at BeforeAssign)[next] ->
                              not prime j) }
        end else begin
          label BeforeAssign in
          t.arr[cnt] <- 2 * p + 1;
          unchanged_other_elements t.arr.elts (pure { t.arr.elts at BeforeAssign })
                                              (to_int cnt) (2 * to_int p + 1);
          cnt <- cnt + 1;
          p <- next;
          assert { forall k. cnt <= k < length (t.arr at BeforeAssign) ->
                             t.arr[k] = (t.arr at BeforeAssign)[k] }
        end
      end else begin
        label BeforeAssign in
        t.arr[cnt] <- 2 * p + 1;
        unchanged_other_elements t.arr.elts (pure { t.arr.elts at BeforeAssign })
                                 (to_int cnt) (2 * to_int p + 1);
        cnt <- cnt + 1;
        p <- t.max_arr + 1;
        assert { forall k. cnt <= k < length (t.arr at BeforeAssign) ->
                           t.arr[k] = (t.arr at BeforeAssign)[k] }
      end
    done;
    sub t.arr 0 cnt

end

download ZIP archive

Why3 Proof Results for Project "euler_sieve"

Theory "euler_sieve.ArithmeticResults": fully verified

ObligationsAlt-Ergo 2.3.3CVC4 1.8
VC for mult_croissance_locale0.00---
VC for mult_croissance0.01---
VC for comp_mult_20.01---
VC for div_croissance_locale1---0.27
VC for div_croissance10.02---
VC for div_croissance_locale2---0.24
VC for div_croissance20.02---
VC for div_mult_1---0.28
VC for mult_borne_sous_exp0.30---
VC for sq_ineq---0.18

Theory "euler_sieve.DivisibilityResults": fully verified

ObligationsAlt-Ergo 2.3.3Vampire 4.2.2
VC for divides_div0.05---
VC for divides_inf0.04---
VC for not_prime_divider_limits0.01---
VC for no_prod_impl_no_divider------
split_vc
postcondition------
case (exists k:int. (2 <= k /\ k < n) /\ not k = i /\ divides k i)
true case (postcondition)------
destruct H
true case (postcondition)------
destruct H
destruct premise------
introduce_exists
destruct premise------
assert (exists l:int. l * k = i)
asserted formula0.02---
destruct premise------
introduce_exists
destruct premise------
exists k
no_prod_impl_no_divider'vc.0.0.0.0.0.1.0.0------
exists l
no_prod_impl_no_divider'vc.0.0.0.0.0.1.0.0.0------
case (l = i)
true case------
assert (k = 1)
asserted formula---0.08
true case0.01---
false case3.40---
true case (postcondition)0.01---
false case (postcondition)0.01---
VC for not_prime_impl_divisor_under_sqrt0.03---

Theory "euler_sieve.EulerSieveSpec": fully verified

ObligationsAlt-Ergo 2.3.3
VC for conservation_all_eliminated_marked_on_marked_change0.06
VC for conservation_all_eliminated_marked_on_nexts_change---
inline_goal
VC for conservation_all_eliminated_marked_on_nexts_change---
split_vc
postcondition---
split_vc
postcondition0.02
postcondition0.53

Theory "euler_sieve.EulerSieve": fully verified

ObligationsAlt-Ergo 2.0.0Alt-Ergo 2.3.3Alt-Ergo 2.4.1CVC3 2.4.1CVC4 1.7CVC4 1.8Eprover 2.0Vampire 4.2.2Z3 3.2Z3 4.8.10
VC for multiples_of_marked_are_marked------------------------------
split_vc
postcondition------------------------------
split_vc
postcondition---0.02------------------------
postcondition---0.01------------------------
postcondition---0.01------------------------
postcondition---0.01------------------------
VC for multiples_of_marked_are_marked------------------------------
inline_all
VC for multiples_of_marked_are_marked---------0.04------------------
remove Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Mod_bound,Div_unique,Div_bound,Mod_1,Div_1,Div_inf,Div_inf_neg,Mod_0,Div_1_left,Div_minus1_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,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,mod_divides_computer,divides_mod_computer,odd_divides,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,H13,H12,Requires,H11,H10,H9,H8,H7,H6,H5,H4,H3,H
VC for multiples_of_marked_are_marked---------0.01---0.03---------0.01
VC for multiples_of_marked_are_marked------------------------------
assert (k * (i * j) = i*j + (k-1)*(i*j))
asserted formula---0.02------------------------
VC for multiples_of_marked_are_marked------------------------------
assert ((k-1)*(i*j) >= 0)
asserted formula---0.02------------------------
VC for multiples_of_marked_are_marked---0.02------------------------
VC for multiples_of_marked_are_marked------------------------------
unfold previously_marked_multiples in Requires
VC for multiples_of_marked_are_marked------------------------------
unfold all_multiples_marked in Requires
VC for multiples_of_marked_are_marked------------------------0.04---
remove zero,one,(-),even,([]),inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,Assoc1,Unit_def_r,Mul_distr_l,Refl,Trans,Div_unique,Div_bound,Div_minus1_left,Div_sign_pos,even_not_odd,odd_not_even,even_odd,odd_2k1,divides_left,divides_oppr_rev,divides_multl,divides_multr,divides_mod_euclidean,mod_divides_computer,prime_divisors,odd_prime,mult_croissance_locale,comp_mult_2,sq_ineq,divides_div,no_prod_impl_no_divider,create'spec,empty'def,set'spec,set'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change
VC for multiples_of_marked_are_marked---------------------0.110.03---
VC for prev_and_new_impl_all_multiples_marked------------------------------
split_vc
assertion------------------------------
split_vc
assertion------------------------------
unfold previously_marked_multiples in Requires2
assertion------------------------------
unfold all_multiples_marked in Requires2
assertion---0.03------------------------
assertion---0.09------------------------
precondition---0.01------------------------
precondition---0.01------------------------
precondition---0.01------------------------
precondition---0.02------------------------
assertion---0.01------------------------
assertion---0.25------------------------
assertion---0.01------------------------
assertion---0.03------------------------
postcondition---0.05------------------------
VC for conservation_only_multiples_marked------------------------------
split_vc
assertion---0.12------------------------
assertion---0.10------------------------
assertion---0.02------------------------
postcondition------------------------------
inline_goal
postcondition------------------------------
split_vc
postcondition------------------------------
case (k = i * j)
true case (postcondition)---0.03------------------------
false case (postcondition)---0.10------------------------
VC for conservation_previously_marked_multiples------------------------------
split_vc
assertion---0.02------------------------
assertion---0.03------------------------
assertion------------------------------
split_vc
assertion---0.02------------------------
VC for conservation_previously_marked_multiples---0.08------------------------
precondition---0.02------------------------
precondition---0.02------------------------
assertion------------------------------
split_vc
assertion---------------------0.50------
VC for conservation_previously_marked_multiples---0.04------------------------
assertion------------------------------
split_vc
assertion------------------------------
inline_goal
assertion------------------------------
split_vc
assertion---0.02------------------------
assertion---0.02------------------------
assertion---0.02------------------------
postcondition---0.02------------------------
conservation_previously_marked_multiples_on_marked_change------------------------------
inline_goal
conservation_previously_marked_multiples_on_marked_change.0------------------------------
split_vc
conservation_previously_marked_multiples_on_marked_change.0.0------------------------------
inline_goal
conservation_previously_marked_multiples_on_marked_change.0.0.0------------------------------
split_vc
conservation_previously_marked_multiples_on_marked_change.0.0.0.0---0.01------------------------
conservation_previously_marked_multiples_on_marked_change.0.0.0.1------------------0.13---------
remove zero,one,(-),(>),(<=),(>=),abs,even,odd,divides,prime,([]),singleton,cons,snoc,(++),inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Unitary,NonTrivialRing,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Mod_bound,Div_unique,Div_bound,Mod_1,Div_inf,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_1_n,divides_0,divides_left,divides_right,divides_oppr,divides_oppl,divides_plusr,divides_minusr,divides_multl,divides_multr,divides_factorl,divides_factorr,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,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,(==)'spec,create'spec,empty'def,set'def,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples
conservation_previously_marked_multiples_on_marked_change.0.0.0.1.0---0.10------------0.030.04------
conservation_previously_marked_multiples_on_marked_change.0.0.0.2------------------------------
inline_all
conservation_previously_marked_multiples_on_marked_change.0.0.0.2.0---------------------------0.43
VC for conservation_not_marked_impl_next_not_marked---0.33------------------------
VC for unchanged_other_elements---0.03------------------------
VC for t------------------------------
split_vc
precondition---0.01------------------------
precondition---0.01------------------------
type invariant---0.02------------------------
type invariant---0.02------------------------
type invariant---0.03------------------------
type invariant---0.04------------------------
type invariant---0.02------------------------
type invariant---0.01------------------------
type invariant---0.03------------------------
VC for remove_products------------------------------
split_vc
division by zero---0.02------------------------
integer overflow---0.04------------------------
precondition---0.02------------------------
precondition---0.02------------------------
assertion------------------------------
split_vc
assertion---0.03------------------------
VC for remove_products---0.08------------------------
VC for remove_products---0.31------------------------
precondition---0.08------------------------
precondition---0.03------------------------
integer overflow---0.08------------------------
precondition------------------------------
split_vc
precondition---0.04------------------------
precondition---0.04------------------------
precondition------------------------------
assert (mod (int63'int n) 2 = 1)
asserted formula---0.32------------------------
precondition---0.04------------------------
precondition------------------------------
split_vc
precondition---0.03------------------------
precondition---0.11------------------------
precondition---0.11------------------------
precondition---0.03------------------------
assertion------------------------------
inline_goal
assertion------------------------------
split_vc
assertion---0.03------------------------
assertion---0.03------------------------
assertion---0.12------------------------
assertion---0.03------------------------
assertion------------------------------
split_vc
assertion---0.03------------------------
assertion---0.13------------------------
VC for remove_products---0.24------------------------
assertion------------------------------
split_vc
assertion---0.03------------------------
assertion---0.03------------------------
assertion---0.14------------------------
VC for remove_products---1.44------------------------
assertion------------------------------
split_vc
assertion------------------------------
inline_goal
assertion------------------------------
split_vc
assertion---0.12------------------------
assertion---0.03------------------------
assertion---0.13------------------------
assertion---0.82------------------------
VC for remove_products1.36---------------------------
assertion------------------------------
split_vc
assertion---------------8.31------------
VC for remove_products---0.64---------0.34------------
precondition---0.03------------------------
precondition---0.04------------------------
assertion---0.12------------------------
precondition---0.03------------------------
precondition---0.04------------------------
precondition------------0.21---------------
precondition---0.04------------------------
precondition---------1.05------------------
precondition---0.04------------------------
precondition---0.04------------------------
precondition---0.17------------------------
precondition---0.04------------------------
assertion------------------------------
inline_goal
assertion------------------------------
split_vc
assertion---0.04------------------------
assertion---0.04------------------------
assertion---0.71------------------------
VC for remove_products---0.15------------------------
VC for remove_products------------------------------
case (j < x)
true case---0.04------------------------
false case------------------------------
unfold all_eliminated_marked_partial in Requires4
false case---------------7.72------------
variant decrease---------------0.46---------0.11
precondition------------------------------
split_vc
precondition---0.04------------------------
precondition---0.04------------------------
precondition---0.04------------------------
precondition---0.04------------------------
precondition---0.04------------------------
precondition---0.04------------------------
precondition---------------0.48---------0.12
precondition---------------0.28---------0.12
precondition---------------0.27---------0.10
precondition------------------------------
split_vc
precondition------------------------------
inline_goal
precondition------------------------------
split_all_full
VC for remove_products---0.16------------------------
VC for remove_products---0.42------------------------
VC for remove_products------------------------------
unfold inv_remove_products in Requires8
VC for remove_products------------------------------
split_premise_right
VC for remove_products------------------------------
inline_goal
VC for remove_products------------------------------
unfold all_primes in Requires11
VC for remove_products------------------------------
split_vc
VC for remove_products------------------------------
instantiate Requires11 i
VC for remove_products---0.56------------------------
VC for remove_products------------------------------
instantiate Requires11 i
VC for remove_products---0.56------------------------
VC for remove_products---0.16------------------------
VC for remove_products---0.40------------------------
VC for remove_products---0.16------------------------
precondition------------0.10---------------
precondition---0.92------------------------
precondition---0.05------------------------
precondition---------------0.29------------
precondition---0.05------------------------
precondition------------------------------
inline_goal
precondition------------------------------
split_vc
precondition---0.16------------------------
precondition---0.16------------------------
precondition---0.04------------------------
precondition------------------------------
case (i = p)
true case (precondition)------------------------------
remove H24,H23,H22
true case (precondition)---2.66------------------------
false case (precondition)------------------------------
assert (forall i. 0 <= i < div (length marked_old - 1) n -> i <> p -> (nexts t)[i] = (nexts t1)[i])
asserted formula---0.20------------------------
false case (precondition)------------------------------
inline_all
false case (precondition)---------------------------3.30
precondition---0.39------------------------
precondition------------------------------
inline_goal
precondition------------------------------
split_vc
precondition---0.16------------------------
precondition---0.17------------------------
precondition---0.04------------------------
precondition---0.19------------------------
precondition------------------------------
unfold not_marked_impl_next_not_marked_partial in Requires8
precondition------------------------------
split_premise_right
precondition------------------------------
instantiate Requires8 i
precondition---------------0.64------------
precondition---0.05------------------------
postcondition---0.04------------------------
postcondition---0.04------------------------
postcondition---0.04------------------------
postcondition---0.04------------------------
postcondition---0.04------------------------
postcondition---0.04------------------------
assertion---------------0.69---------0.09
variant decrease------------------------------
split_vc
variant decrease---0.03------------------------
variant decrease---------------0.36---------0.10
precondition------------------------------
split_vc
precondition---0.03------------------------
precondition---0.03------------------------
precondition---0.04------------------------
precondition---0.04------------------------
precondition---0.03------------------------
precondition---0.03------------------------
precondition---------------0.38---------0.08
precondition---0.03------------------------
precondition---------------0.25---------0.09
precondition------------------------------
split_vc
precondition------------------------------
inline_goal
precondition------------------------------
split_all_full
VC for remove_products---0.13------------------------
VC for remove_products---0.29------------------------
VC for remove_products------------------------------
unfold inv_remove_products in Requires8
VC for remove_products------------------------------
split_premise_right
VC for remove_products------------------------------
inline_goal
VC for remove_products------------------------------
unfold all_primes in Requires11
VC for remove_products------------------------------
split_vc
VC for remove_products------------------------------
instantiate Requires11 i
VC for remove_products---0.36------------------------
VC for remove_products------------------------------
instantiate Requires11 i
VC for remove_products---0.34------------------------
VC for remove_products---0.14------------------------
VC for remove_products---0.27------------------------
VC for remove_products---0.13------------------------
precondition------------0.08---------------
precondition---0.64------------------------
precondition---0.04------------------------
precondition---0.74------------------------
precondition---------------------------0.10
precondition---0.04------------------------
precondition---0.04------------------------
precondition------------------------------
inline_goal
precondition------------------------------
split_vc
precondition---0.14------------------------
precondition---0.14------------------------
precondition---0.04------------------------
precondition---0.17------------------------
precondition------------------------------
unfold not_marked_impl_next_not_marked_partial in Requires8
precondition------------------------------
split_premise_right
precondition------------------------------
instantiate Requires8 i
precondition---------------0.52------------
precondition---0.04------------------------
postcondition---0.04------------------------
postcondition---0.04------------------------
postcondition---0.03------------------------
postcondition---0.04------------------------
postcondition---0.03------------------------
postcondition---0.03------------------------
assertion------------------------------
split_vc
assertion---0.03------------------------
VC for remove_products---------------------------0.08
VC for remove_products---0.59------------------------
VC for remove_products---0.12------------------------
VC for remove_products---0.10------------------------
precondition------------------------------
split_vc
precondition---------------0.24---------0.06
precondition---0.03------------------------
VC for remove_products---0.76------------------------
VC for remove_products---------------0.29---------0.07
VC for remove_products---0.03------------------------
VC for remove_products---------------------------0.09
postcondition---0.03------------------------
postcondition---0.02------------------------
postcondition---0.03------------------------
postcondition---0.02------------------------
postcondition------------------------------
inline_goal
postcondition------------------------------
split_vc
postcondition---0.06------------------------
postcondition---0.07------------------------
postcondition---0.03------------------------
postcondition------------------------------
unfold prime_multiples_marked in Requires2
postcondition------------------------------
split_all_right
postcondition------------------------------
case (i < (nexts t)[x])
true case (postcondition)---0.08------------------------
false case (postcondition)---0.16------------------------
postcondition---0.03------------------------
precondition------------------------------
split_vc
precondition---------------0.25---------0.07
precondition---0.03------------------------
VC for remove_products------1.59---------------------
VC for remove_products---------------0.29---------0.08
VC for remove_products---0.02------------------------
VC for remove_products---------------------------0.09
postcondition---0.02------------------------
postcondition---0.02------------------------
postcondition---0.03------------------------
postcondition---0.03------------------------
postcondition---0.06------------------------
postcondition---0.03------------------------
precondition---0.03------------------------
precondition0.04---------------------------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,max,marked_old,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,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,to_int_in_bounds,extensionality,max_int'def,min_int'def,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,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,t'invariant,H2,H1,H,Requires4,Requires3,Requires1,Ensures1,Ensures,Requires
precondition0.000.00---------------------0.02
integer overflow---0.03------------------------
precondition---0.02------------------------
precondition------------------------------
assert (mod (int63'int n) 2 = 1)
asserted formula---------------0.17---------0.06
precondition---0.08------------------------
precondition---0.04------------------------
precondition---0.02------------------------
assertion------------------------------
split_vc
assertion---0.06------------------------
assertion---------------0.22------------
VC for remove_products---------------0.17---------0.07
VC for remove_products---0.04------------------------
VC for remove_products---0.04------------------------
precondition------------------------------
split_vc
precondition---0.02------------------------
precondition---0.02------------------------
precondition---0.02------------------------
precondition---0.02------------------------
precondition---------------0.20---------0.06
precondition---0.02------------------------
precondition---------------0.24---------0.07
precondition---0.02------------------------
precondition---------------------------0.08
precondition------------------------------
inline_goal
precondition------------------------------
split_vc
precondition---------------0.18---------0.07
precondition---------------------------0.06
precondition------------------------------
assert (n * n > n)
asserted formula---------------------------0.07
precondition---------------0.22------------
precondition---------------0.15---------0.06
precondition---------------------------0.07
precondition---------------0.16---------0.06
precondition---------------------------0.08
precondition---------------0.14---------0.07
precondition---------------0.22------------
precondition---------2.11------------------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),inv_nexts,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,max,marked_copy,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,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,to_int_in_bounds,extensionality,max_int'def,min_int'def,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,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,H4,H3,H2,Requires8,Requires7,Requires6,Requires5,Ensures5,Ensures4,Ensures3,Ensures2,H,Ensures1,Ensures,Assert,Requires3,Requires2,Requires1,Requires
precondition---0.10---0.02---0.06------------
precondition------------------------------
inline_goal
precondition------------------------------
split_vc
precondition---------------0.15---------0.06
precondition---------------0.18---------0.06
precondition---0.02---------0.15------------
precondition---------------------------0.07
precondition------------------------------
split_vc
precondition------------------------------
inline_goal
precondition------------------------------
split_all_full
VC for remove_products---------------0.20---------0.08
VC for remove_products---0.02---------0.11------------
VC for remove_products---------------0.28---------0.08
VC for remove_products---------------0.26------------
precondition------------------------------
inline_goal
precondition------------------------------
split_vc
precondition---------------0.15---------0.08
precondition---------------0.18---------0.06
precondition---0.02---------0.15---------0.06
precondition---------------------------0.06
precondition------------------------------
inline_all
precondition---------------------------0.24
precondition---0.02---------0.15---------0.07
precondition---0.05---------0.18---------0.06
precondition---0.02---------0.11---------0.02
precondition---0.02---------0.11---------0.02
precondition---0.02---------0.11---------0.02
precondition---0.02---------0.10---------0.02
precondition---0.02---------0.12---------0.02
precondition---------------0.28---------0.07
precondition---0.02---------0.12---------0.02
precondition---0.02---------0.12---------0.02
precondition---0.05---------0.20---------0.07
precondition---0.02---------0.12---------0.02
precondition---0.02---------0.11---------0.02
postcondition---0.02---------0.12---------0.01
postcondition---0.02---------0.11---------0.02
postcondition---0.02---------0.11---------0.02
postcondition------------------------------
inline_goal
postcondition------------------------------
split_vc
postcondition------------------------------
unfold only_multiples_marked in Ensures5
postcondition------------------------------
instantiate Ensures5 k
postcondition0.71---------------------------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,max,marked_old,marked_copy,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,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,to_int_in_bounds,extensionality,max_int'def,min_int'def,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,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,H8,H6,Requires3,Requires2,Requires1,Requires,Ensures16,Ensures15,Ensures14,Ensures13,H5,Ensures12,Ensures11,Assert,Ensures10,Ensures9,Ensures8,Ensures7,Ensures6,Ensures5,Ensures4,Ensures3,Ensures2,Ensures1,Ensures
postcondition0.060.05---------------------0.02
VC for previously_marked_multiples_impl_prime------------------------------
split_vc
assertion------------------------------
split_vc
assertion------------------------------
inline_all
assertion---------------------------0.10
VC for previously_marked_multiples_impl_prime---0.42------------------------
postcondition---0.03---------0.16---------0.06
VC for only_multiples_marked_impl_not_marked------------------------------
split_vc
assertion---0.03------------------------
postcondition---0.48------------------------

Theory "euler_sieve.EulerSieveImpl": fully verified

ObligationsAlt-Ergo 2.0.0Alt-Ergo 2.3.3CVC3 2.4.1CVC4 1.8Vampire 4.2.2Z3 4.8.10
VC for conservation_inv_arr_on_mark------------------
split_vc
assertion---0.30---0.15------
assertion---0.32---0.15---0.06
postcondition------------------
assert (abs arr[i] = abs arr[i <- - arr[i]][i])
asserted formula---0.16---0.16---0.05
postcondition------------------
case (j = i)
true case (postcondition)---0.23---0.16------
false case (postcondition)---1.80---0.19------
VC for conservation_inv_arr_on_jump------------------
split_vc
precondition---0.02---0.10---0.02
precondition---0.02---0.13---0.06
assertion---2.26---0.15------
assertion---3.29---0.16------
postcondition---4.87------------
VC for t------------------
split_vc
array creation size---0.01---0.09---0.02
index in array bounds---0.02---0.11---0.01
precondition---0.01---0.10---0.02
precondition---0.02---0.12---0.02
type invariant---0.01---0.12---0.02
type invariant---0.02---0.24------
type invariant---0.00---0.12---0.02
type invariant---0.02---0.11---0.02
type invariant---0.04---0.19------
type invariant---0.04---0.88------
type invariant---0.01---0.15---0.03
type invariant---0.04---0.20------
type invariant---0.13---0.14------
type invariant---------0.21------
type invariant---2.88---0.25------
type invariant---0.29---0.21---0.10
type invariant---4.09---0.21---0.33
type invariant---------0.21------
type invariant---4.92---0.24------
VC for create------------------
split_vc
integer overflow---0.02---0.14---0.05
division by zero---0.02---0.10---0.02
integer overflow---0.04---0.14---0.06
integer overflow---0.04---0.14---0.05
precondition---0.02---0.12---0.05
precondition---0.02---0.11---0.02
precondition---0.02---0.15---0.06
array creation size---0.03---0.20---0.08
integer overflow---0.03---0.17---0.08
loop invariant init---0.05---0.20------
integer overflow---0.04---0.18---0.07
integer overflow---0.04---0.20---0.08
integer overflow---0.04---0.19---0.08
integer overflow---0.04---0.19---0.08
index in array bounds---0.03---0.17---0.08
loop invariant preservation---4.32---0.22------
integer overflow---0.03---0.20---0.07
division by zero---0.02---0.12---0.02
integer overflow---0.04---0.20---0.08
precondition---0.02---0.12---0.02
precondition---0.02---0.15---0.07
precondition---0.05---0.22------
precondition---0.06---0.20---0.08
precondition---------0.22------
precondition---------0.36------
precondition---0.06---0.21---0.08
precondition---0.11---0.22------
precondition---0.53---0.26------
precondition---1.28---0.25------
precondition---0.65---0.24------
precondition---1.08---0.26------
precondition---1.07---0.26------
precondition---4.96---0.25------
precondition---------0.26------
postcondition---0.02---0.13---0.02
postcondition---0.30---0.23------
postcondition---0.49---0.24------
postcondition---0.07---0.25---0.08
postcondition---1.10---0.26---0.09
postcondition---1.24---0.26---0.09
postcondition---0.49---0.25---0.09
out of loop bounds---0.05---0.21---0.08
VC for set_next------------------
split_vc
precondition---0.03---0.20---0.07
precondition---0.03---0.18---0.07
precondition---0.04---0.19---0.07
precondition---0.03---0.20---0.06
precondition---0.04---0.18---0.07
precondition---0.04---0.18---0.07
division by zero---0.02---0.10---0.02
integer overflow---0.09---0.16---0.06
index in array bounds---0.05---0.21---0.07
precondition---0.05---0.19---0.07
type invariant---0.05---0.19---0.08
type invariant---0.05---0.18---0.06
type invariant---0.06---0.19---0.07
type invariant---0.06---0.19---0.08
type invariant---------0.26------
type invariant---0.06---0.20------
type invariant---0.07---0.22---0.08
type invariant---1.18---0.27------
type invariant---0.32---0.23------
type invariant---------0.24------
type invariant---------0.31------
type invariant---------0.30------
type invariant---------0.27------
type invariant---------0.23------
type invariant---------0.30------
postcondition---0.02---0.12---0.04
VC for get_next------------------
split_vc
division by zero---0.02---0.09---0.02
integer overflow---0.06---0.14---0.06
index in array bounds---0.04---0.17---0.07
index in array bounds---0.05---0.18---0.07
integer overflow---0.05---0.19------
index in array bounds---0.04---0.18---0.07
postcondition---0.64---0.22------
postcondition---0.08---0.46------
postcondition------------------
assert (i >= 3)
asserted formula---0.02---0.10---0.02
postcondition------------------
case (i < max t - 1)
true case (postcondition)---0.05---0.20---0.06
false case (postcondition)------------------
case (i = max t)
false case (true case. postcondition)---0.05---0.14---0.06
false case (postcondition)---0.10---0.26---0.12
VC for set_mark------------------
split_vc
division by zero---0.02---0.10---0.02
integer overflow---0.06---0.16---0.06
precondition---0.03---0.19---0.06
precondition---0.04---0.19---0.07
precondition---0.03---0.18---0.06
precondition---0.04---0.18---0.07
index in array bounds---0.04---0.18---0.06
precondition---0.07---0.27---0.08
precondition---0.14---0.22------
precondition---0.05---0.19---0.07
precondition---0.01---0.15---0.06
index in array bounds---0.04---0.19---0.06
integer overflow---0.04---0.17---0.06
index in array bounds---0.05---0.19---0.07
precondition---0.05---0.20---0.07
type invariant---0.05---0.20---0.07
type invariant---0.05---0.19---0.07
type invariant---0.06---0.19---0.08
type invariant---0.06---0.21---0.08
type invariant---0.06---0.18---0.08
type invariant---0.06---0.20------
type invariant---0.42---0.23------
type invariant---0.08---0.24---0.08
type invariant---0.06---0.20---0.07
type invariant---------0.26------
type invariant---------0.26------
type invariant---------0.28------
type invariant---------0.32------
type invariant---------0.22------
type invariant---0.12---0.37------
postcondition---0.02---0.12---0.04
precondition---0.04---0.18---0.07
type invariant---0.04---0.18---0.08
type invariant---0.05---0.20---0.07
type invariant---0.05---0.20---0.08
type invariant---0.06---0.19---0.08
type invariant---0.06---0.20---0.07
type invariant---0.06---0.20------
type invariant---0.41---0.24------
type invariant---0.07---0.20---0.08
type invariant---0.07---0.21---0.08
type invariant---0.08---0.20------
type invariant---0.22---0.27------
type invariant---0.07---0.23---0.08
type invariant---0.08---0.27---0.09
type invariant---0.10---0.23------
type invariant---0.11---0.33---0.09
postcondition---0.02---0.12---0.04
VC for get_mark---0.20------------
VC for get_max---0.03---0.14---0.06
VC for t------------------
split_vc
VC for t---0.02---0.13---0.06
VC for t---0.03---0.14---0.05
VC for t---0.03---0.17---0.07
VC for t---0.02---0.17---0.06
VC for t---0.02---0.16---0.06
VC for t---0.03---0.14---0.05
VC for t---0.03---0.16---0.07
VC for t---0.04---0.18---0.06
VC for t---0.03---0.16---0.06
VC for t---0.03---0.16---0.06
VC for t---0.03---0.16---0.06
VC for create'refn------------------
split_vc
precondition---0.02---0.10---0.02
postcondition---0.02---0.12---0.02
postcondition---0.02---0.12---0.02
postcondition---0.04---0.30------
postcondition---0.04---------0.07
postcondition---0.04---------0.07
postcondition---0.03---0.20---0.08
VC for set_next'refn---0.10---0.16------
VC for get_next'refn---0.02---0.13---0.05
VC for set_mark'refn---0.03---0.18---0.06
VC for get_mark'refn---0.02---0.13---0.05
VC for get_max'refn---0.02---0.10---0.01
VC for euler_sieve------------------
split_vc
precondition---0.02---0.10---0.02
precondition---0.02---0.18---0.06
precondition---0.02---0.13---0.02
precondition---0.02---0.14---0.02
precondition---0.02---0.12---0.02
precondition---0.02---0.13---0.02
precondition---0.02---0.18---0.04
precondition---0.19---0.27---0.08
division by zero---0.03---0.18---0.02
integer overflow---0.18---0.22---0.09
assertion---0.46------------
precondition------------------
split_vc
precondition---0.02---0.18---0.08
precondition---0.06---0.24---0.08
precondition------------------
unfold not_marked_impl_next_not_marked in Ensures5
precondition------------------
split_premise_right
precondition------------------
assert (int63'int nn <= div (int63'int (max1 t)) (int63'int nn))
asserted formula---0.10---------0.10
precondition---------------0.13
precondition---0.03---0.19---0.09
assertion------------------
split_vc
assertion---------0.33---0.26
VC for euler_sieve------------------
unfold only_multiples_marked in Ensures4
VC for euler_sieve------------------
remove zero1,one1,(-),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,singleton,cons,snoc,(++),exchange,all_eliminated_marked_partial,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,inv_count,Assoc1,Unit_def_l,Unit_def_r,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Refl,CompatOrderAdd,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,to_int_in_bounds,extensionality,max_int'def,min_int'def,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,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,exchange_set,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,array63'invariant,conservation_inv_arr_on_mark,conservation_inv_arr_on_jump,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,previously_marked_multiples_impl_prime,only_multiples_marked_impl_not_marked,H18,H17,Ensures13,H16,H15,H14,Ensures12,Ensures11,Ensures10,Ensures9,Ensures8,H13,H10,H9,Requires4,Requires3,Requires2,Requires,H8,Ensures7,Ensures6,Ensures5,H5,Ensures2,Ensures1,H3,Assert,Ensures,H12,H11,H7,H6
VC for euler_sieve---0.05---------0.03
VC for euler_sieve------------9.99---
variant decrease---4.61---0.33---0.10
precondition---0.02---0.23---0.09
precondition---0.03---0.12---0.02
precondition---0.03---0.18---0.08
precondition---0.03---0.16---0.09
precondition------------------
split_vc
precondition------------------
inline_goal
precondition------------------
split_all_full
VC for euler_sieve---0.07---0.21---0.10
VC for euler_sieve---0.07---0.28---0.10
VC for euler_sieve---0.03---0.18---0.08
VC for euler_sieve---1.50---------0.12
precondition------------------
inline_goal
precondition------------------
split_vc
precondition---0.07---0.18---0.09
precondition---0.07---0.17---0.09
precondition---------1.06------
precondition---0.03---0.14---0.02
precondition------------------
unfold not_marked_impl_next_not_marked in Requires
precondition------------------
split_premise_right
precondition------------------
assert (int63'int nn <= div (int63'int (max1 t)) (int63'int nn))
asserted formula---0.11---------0.10
precondition---------------0.14
precondition---0.07---0.18---0.08
postcondition---0.12---0.26------
precondition---0.03---0.17---0.07
assertion------------------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,singleton,cons,snoc,(++),exchange,inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,inv_count,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Refl,Trans,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,to_int_in_bounds,extensionality,max_int'def,min_int'def,even_or_odd,even_not_odd,odd_not_even,even_odd,odd_even,even_even,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,odd_divides,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,exchange_set,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,array63'invariant,conservation_inv_arr_on_mark,conservation_inv_arr_on_jump,t'invariant,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,previously_marked_multiples_impl_prime,only_multiples_marked_impl_not_marked,H17,H16,H15,Ensures13,H14,H13,H12,Ensures12,Ensures11,Ensures10,Ensures9,Ensures8,H11,H10,H9,H8,Requires4,Requires3,Requires2,Requires1,Requires,H7,H6,Ensures7,Ensures6,Ensures4,H5,H4,Ensures2,Ensures1,H3,Ensures,H2
assertion---0.03------0.08---
precondition---0.02---0.17---0.08
assertion------------------
split_vc
assertion---0.07------------
VC for euler_sieve---------------0.10
VC for euler_sieve---0.91---------0.08
VC for euler_sieve---0.10------------
VC for euler_sieve---0.03---0.17---0.08
VC for euler_sieve---0.07---0.23---0.09
assertion------------------
split_vc
assertion---0.66------------
assertion---0.73------------
VC for euler_sieve---0.68------------
VC for euler_sieve---0.08---------0.08
VC for euler_sieve---0.57------------
VC for euler_sieve---0.46---0.29---0.11
postcondition------------------
split_vc
postcondition---2.20---0.31---0.10
postcondition------------------
assert (forall j k. 2 <= j < (nexts t)[n] -> 2 <= k < length (marked t) -> j * k <> i)
asserted formula---0.47------------
postcondition---------0.29------
precondition---0.02---0.13---0.02
precondition---0.02---0.12---0.01
precondition---0.15------------
precondition0.70---------------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,divides,prime,singleton,cons,snoc,(++),exchange,inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,inv_count,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,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,to_int_in_bounds,extensionality,max_int'def,min_int'def,even_or_odd,even_not_odd,odd_not_even,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,odd_divides,not_prime_1,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,exchange_set,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,array63'invariant,conservation_inv_arr_on_mark,conservation_inv_arr_on_jump,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,previously_marked_multiples_impl_prime,only_multiples_marked_impl_not_marked,H6,H5,H4,H3,H2,Ensures4,Ensures3,Ensures2,Ensures1,H,Requires2,Requires1,Requires
precondition0.030.11---0.06------
precondition------------------
inline_goal
precondition------------------
split_vc
precondition---0.03---0.22---0.08
precondition---0.03---0.20---0.07
precondition---0.02---0.13---0.02
precondition------------------
case (mod i 2 = 0)
true case (precondition)------------------
case (i < max - 1)
true case (precondition)------------------
instantiate Ensures1 i
true case (precondition)---------0.43---0.10
false case (true case. precondition)---0.06---0.21---0.08
false case (precondition)---0.18---0.30------
precondition---0.72---0.36------
assertion---0.09---0.24------
assertion------------------
case (mod i 2 = 0)
true case (assertion)---0.19---0.24---0.08
false case (assertion)------------------
split_vc
VC for euler_sieve---0.03---0.13---0.02
VC for euler_sieve---0.03---0.14---0.02
VC for euler_sieve---0.80---0.46------
assertion---2.14---0.26------
index in array bounds---0.04---0.21---0.08
loop invariant init---0.04---0.21---0.08
loop invariant init---0.02---0.14---0.02
loop invariant init---0.17---0.25---0.10
loop invariant init---0.02---0.14---0.02
loop invariant init------------------
inline_goal
loop invariant init------------------
split_vc
loop invariant init------------------
assert (forall i. 1 <= i < length (arr t)[0 <- 2] -> (arr t)[i] = (arr t)[0 <- 2][i])
asserted formula---0.05---0.21---0.09
loop invariant init---0.39---0.26---0.10
loop invariant init---0.60---0.26---0.10
loop invariant init---0.22---0.26---0.10
loop invariant init---0.12---0.25---0.09
loop invariant init------------------
assert (forall i. 1 <= i < length (arr t)[0 <- 2] -> (arr t)[i] = (arr t)[0 <- 2][i])
asserted formula---0.06---0.23---0.09
loop invariant init---0.63---0.31------
loop invariant init---0.32---0.38---0.10
loop invariant init---0.05---0.21---0.08
loop invariant init---0.18---0.24------
loop invariant init---0.06---0.27------
loop invariant init---0.14---0.24---0.09
loop invariant init---0.54---0.27---0.12
integer overflow---0.05---0.22---0.08
integer overflow---0.04---0.23------
index in array bounds---0.05---0.25---0.09
division by zero---0.02---0.13---0.02
integer overflow---0.11---0.24------
assertion---0.06---0.23------
index in array bounds---0.07---0.25---0.09
index in array bounds---0.06---0.24---0.10
integer overflow---0.27---0.30------
index in array bounds---0.06---0.24---0.10
index in array bounds---0.07---0.24---0.12
precondition---0.07---0.26---0.10
precondition---0.72---0.32------
assertion------------------
split_vc
assertion------------------
unfold inv_count in LoopInvariant5
assertion------------------
instantiate LoopInvariant5 (int63'int p)
assertion------------------
instantiate LoopInvariant5 (int63'int next)
assertion---------0.36------
assertion------------------
split_vc
assertion---1.34---0.30---0.18
assertion---1.53---0.37------
assertion---0.79---0.29---0.11
precondition---0.03---0.20---0.08
precondition---------------0.13
precondition---1.32---0.31------
precondition---0.09---0.25---0.10
precondition---0.11---0.41------
precondition---0.14---0.46------
assertion---0.39---0.30------
assertion------------------
unfold inv_count in LoopInvariant5
assertion------------------
split_vc
assertion---0.56---2.21------
assertion---0.54---------0.12
loop variant decrease---0.08---0.34---0.12
loop invariant preservation---0.03---0.15---0.02
loop invariant preservation---0.03---0.14---0.02
loop invariant preservation---0.03---0.18---0.09
loop invariant preservation---0.03---0.14---0.02
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation------------------
case (i <> p)
true case (loop invariant preservation)---1.08---0.32------
false case (loop invariant preservation)---1.31---0.30------
loop invariant preservation------------------
case (i <> p)
true case (loop invariant preservation)---1.05---0.32---0.22
false case (loop invariant preservation)---0.93---0.32---0.14
loop invariant preservation---1.52---0.33------
loop invariant preservation---0.52---0.32---0.13
loop invariant preservation---1.01------------
loop invariant preservation------------------
case (i <> p)
true case (loop invariant preservation)------0.14---------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,Refl,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,to_int_in_bounds,extensionality,max_int'def,min_int'def,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,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,exchange_set,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,conservation_inv_arr_on_mark,conservation_inv_arr_on_jump,t'invariant,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,previously_marked_multiples_impl_prime,only_multiples_marked_impl_not_marked,H39,H38,Ensures18,H37,H36,H35,Ensures17,Ensures16,Ensures15,Ensures14,Ensures13,H34,H33,Ensures12,Assert3,Assert2,Assert1,H30,H29,Ensures11,H28,H27,H26,H25,H24,LoopInvariant9,LoopInvariant8,LoopInvariant6,LoopInvariant5,LoopInvariant4,LoopInvariant3,LoopInvariant2,Ensures10,Ensures9,H23,Ensures8,Ensures7,H22,Ensures6,H17,Ensures5,Ensures4,H16,Ensures3,Ensures2,Assert,Ensures,LoopInvariant1,LoopInvariant,H32,H31,H21,H20,H19,H18,H14,H13,H12,H11,H10,H9,H8,H7,H6,H4
true case (loop invariant preservation)---0.020.020.04---0.02
false case (loop invariant preservation)---1.22---0.39------
loop invariant preservation---------0.46------
loop invariant preservation---------0.44------
loop invariant preservation---0.29---0.30------
loop invariant preservation---1.10---0.31------
loop invariant preservation------------------
instantiate LoopInvariant9 i
loop invariant preservation---1.46---0.34------
integer overflow---0.06---0.18---0.10
integer overflow---0.06---0.25---0.08
index in array bounds---0.06---0.24---0.10
precondition---0.07---0.25---0.10
precondition---0.03------------
integer overflow---0.06---0.23---0.10
assertion---0.15---0.25---0.11
loop variant decrease---------0.38---0.11
loop invariant preservation---0.32---0.35---0.11
loop invariant preservation---0.38---0.40---0.11
loop invariant preservation---0.10---0.26---0.10
loop invariant preservation---0.08---0.26---0.10
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation---1.90---0.32---0.13
loop invariant preservation---------0.32---0.13
loop invariant preservation---0.52---0.32---0.11
loop invariant preservation---0.41---0.33---0.12
loop invariant preservation------------------
unfold inv_count in LoopInvariant7
loop invariant preservation------------------
split_premise_right
loop invariant preservation------------------
assert (t_arr[cnt1 <- ((2 * p1) + 1)][i] = t_arr[i])
asserted formula---------0.41------
loop invariant preservation------------------
instantiate LoopInvariant9 i
loop invariant preservation------------------
assert (cnt1 <= i < length t_arr1)
asserted formula---0.12---0.24---0.12
loop invariant preservation------2.68---------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),exchange,inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,inv_count,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_pos,Div_mod,Div_unique,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_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,to_int_in_bounds,extensionality,max_int'def,min_int'def,even_or_odd,even_not_odd,odd_not_even,even_odd,odd_even,even_even,odd_odd,even_2k,odd_2k1,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,not_prime_1,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,empty'def,set'def,([<-])'def,([..])'def,([_..])'def,([.._])'def,exchange_set,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,conservation_inv_arr_on_mark,conservation_inv_arr_on_jump,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,previously_marked_multiples_impl_prime,only_multiples_marked_impl_not_marked,H33,H32,Ensures18,H31,H30,H29,Ensures17,Ensures16,Ensures15,Ensures14,Ensures13,H28,H27,Assert2,Assert1,H24,H23,Ensures10,H22,H21,H20,H19,H18,LoopInvariant15,LoopInvariant14,LoopInvariant7,LoopInvariant6,LoopInvariant3,LoopInvariant2,Ensures9,Ensures8,H17,Ensures7,Ensures6,H16,Ensures5,H11,Ensures4,Ensures3,H10,H9,Ensures2,Ensures1,Ensures,H8,LoopInvariant1,LoopInvariant,H26,H25,H15,H14,H13,H12,H7,H6,H5,H4,H2,(==)'spec3,(==)'spec2,(==)'spec1,(==)'spec,create'spec1,create'spec,set'spec2,set'spec1,set'spec,singleton'spec1,singleton'spec,cons'spec2,cons'spec1,cons'spec,snoc'spec2,snoc'spec1,snoc'spec,([..])'spec1,([..])'spec,(++)'spec2,(++)'spec1,(++)'spec,Abs_le2,Abs_le1,Abs_le,Div_bound3,Div_bound2,Mod_bound3,Mod_bound2,array63'invariant3,array63'invariant2,array63'invariant1,array63'invariant,Mod_bound1,Mod_bound,Div_bound1,Div_bound,divides'spec1,divides'spec,even_mod21,even_mod2,even_divides1,even_divides,odd_divides1,odd_divides,div_mult_11,div_mult_1,mult_borne_sous_exp1,mult_borne_sous_exp,t'invariant22,t'invariant21,t'invariant20,t'invariant19,t'invariant18,t'invariant17,t'invariant16,t'invariant15,t'invariant14,t'invariant13,t'invariant12,t'invariant11,t'invariant10,t'invariant9,t'invariant8,t'invariant7,t'invariant6,t'invariant5,t'invariant4,t'invariant3,t'invariant2,t'invariant1,t'invariant,Ensures12,Ensures11,Assert4,Assert3,LoopInvariant13,LoopInvariant11,LoopInvariant10,LoopInvariant9,LoopInvariant8,LoopInvariant5,LoopInvariant4,h1
loop invariant preservation---0.020.010.04---0.02
loop invariant preservation---------------0.18
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation------------------
case (j = cnt1)
true case (loop invariant preservation)------2.79---------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),exchange,inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,inv_count,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,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,to_int_in_bounds,extensionality,max_int'def,min_int'def,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,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,exchange_set,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,conservation_inv_arr_on_mark,conservation_inv_arr_on_jump,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,previously_marked_multiples_impl_prime,only_multiples_marked_impl_not_marked,H32,H31,Ensures17,H30,H29,H28,Ensures16,Ensures15,Ensures14,Ensures13,Ensures12,H27,H26,Ensures11,Assert3,Assert2,Assert1,H23,H22,H20,H19,H18,H17,LoopInvariant10,LoopInvariant9,LoopInvariant8,LoopInvariant7,LoopInvariant5,LoopInvariant4,LoopInvariant3,Ensures9,Ensures8,H16,Ensures7,Ensures6,H15,Ensures5,H10,H9,H8,Ensures1,Ensures,H7,Assert,LoopInvariant2,LoopInvariant1,LoopInvariant,H25,H24,H14,H13,H12,H11,H6,H4
true case (loop invariant preservation)---0.080.10------0.02
false case (loop invariant preservation)---1.38---0.33------
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation------------------
unfold all_inf_or_eq in LoopInvariant7
loop invariant preservation------------------
instantiate LoopInvariant7 i
loop invariant preservation------------------
unfold inv_count in LoopInvariant1
loop invariant preservation------------------
split_premise_right
loop invariant preservation------------------
instantiate LoopInvariant6 (int63'int p1)
loop invariant preservation---------0.62------
loop invariant preservation---0.27---0.34------
loop invariant preservation------------------
instantiate LoopInvariant9 i
loop invariant preservation---1.60------------
loop invariant preservation------------------
case (i < 2 * p1 + 1)
true case (loop invariant preservation)------------------
instantiate LoopInvariant9 i
true case (loop invariant preservation)---0.74---0.33------
false case (loop invariant preservation)------------------
case (i = 2 * p1 + 1)
false case (true case. loop invariant preservation)---------0.49---0.30
false case (loop invariant preservation)------2.07---------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),exchange,inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,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,Div_11,Mod_11,Div_inf1,Mod_inf,Div_mult1,Mod_mult1,to_int_in_bounds,extensionality,max_int'def,min_int'def,even_or_odd,even_not_odd,odd_not_even,even_odd,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,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,exchange_set,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,conservation_inv_arr_on_mark,conservation_inv_arr_on_jump,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,previously_marked_multiples_impl_prime,only_multiples_marked_impl_not_marked,H24,H23,H22,Ensures17,H21,H20,H19,Ensures16,Ensures15,Ensures14,Ensures13,Ensures12,H18,H17,H16,Ensures11,Assert4,Assert3,Assert2,H15,Ensures10,H12,H11,H10,LoopInvariant16,LoopInvariant15,LoopInvariant13,LoopInvariant12,LoopInvariant11,LoopInvariant10,LoopInvariant9,Ensures9,Ensures8,H8,Ensures4,Ensures3,H5,H4,Ensures2,Ensures1,Ensures,LoopInvariant8,LoopInvariant6,LoopInvariant5,LoopInvariant4,LoopInvariant3,LoopInvariant2,LoopInvariant,H2
false case (loop invariant preservation)------0.05---------
remove zero1,one1,(-),(>),(<=),(>=),int63'maxInt,int63'minInt,min_int63,max_int63,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),exchange,inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,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,to_int_in_bounds,extensionality,max_int'def,min_int'def,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,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,div_mult_1,mult_borne_sous_exp,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,exchange_set,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,conservation_inv_arr_on_mark,conservation_inv_arr_on_jump,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,previously_marked_multiples_impl_prime,only_multiples_marked_impl_not_marked,H24,H23,H22,Ensures17,H21,H20,H19,Ensures16,Ensures15,Ensures14,Ensures13,Ensures12,H18,H17,H16,Assert4,Assert3,Assert2,H15,Ensures10,H12,H11,H10,LoopInvariant16,LoopInvariant15,LoopInvariant13,LoopInvariant12,LoopInvariant11,LoopInvariant10,LoopInvariant9,Ensures9,Ensures8,H8,Ensures5,H6,Ensures4,Ensures3,H5,H4,Ensures2,Ensures1,Ensures,Assert,LoopInvariant8,LoopInvariant7,LoopInvariant6,LoopInvariant5,LoopInvariant4,LoopInvariant3,LoopInvariant2,LoopInvariant1,LoopInvariant,H2
false case (loop invariant preservation)---0.18------------
integer overflow---0.06---0.19---0.08
integer overflow---0.06---0.24---0.09
index in array bounds---0.07---0.26---0.09
precondition---0.07---0.25---0.10
precondition---0.03---0.31------
integer overflow---0.06---0.24---0.09
integer overflow---0.07---0.24---0.10
assertion---0.14---0.26---0.10
loop variant decrease---0.07---0.28---0.10
loop invariant preservation---0.02---0.18---0.08
loop invariant preservation---0.06---0.27---0.10
loop invariant preservation---0.08---0.26---0.08
loop invariant preservation---0.08---0.26---0.10
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation---3.01---0.32---0.12
loop invariant preservation---------0.31---0.13
loop invariant preservation---0.69---0.30---0.12
loop invariant preservation---0.35---0.32---0.11
loop invariant preservation------------------
unfold inv_count in LoopInvariant7
loop invariant preservation------------------
split_premise_right
loop invariant preservation------------------
assert (t_arr[cnt1 <- ((2 * p1) + 1)][i] = t_arr[i])
asserted formula---------0.42------
loop invariant preservation------------------
instantiate LoopInvariant9 i
loop invariant preservation------------------
assert (cnt1 <= i < length t_arr1)
asserted formula---0.12---0.23---0.13
loop invariant preservation------1.38---------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),exchange,inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,inv_count,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_pos,Div_mod,Div_unique,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_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,to_int_in_bounds,extensionality,max_int'def,min_int'def,even_or_odd,even_not_odd,odd_not_even,even_odd,odd_even,even_even,odd_odd,even_2k,odd_2k1,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,not_prime_1,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,empty'def,set'def,([<-])'def,([..])'def,([_..])'def,([.._])'def,exchange_set,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,conservation_inv_arr_on_mark,conservation_inv_arr_on_jump,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,previously_marked_multiples_impl_prime,only_multiples_marked_impl_not_marked,H27,H26,Ensures18,H25,H24,H23,Ensures17,Ensures16,Ensures15,Ensures14,Ensures13,H22,H21,Assert2,Assert1,H18,H17,Ensures10,H16,H15,H14,H13,H12,LoopInvariant15,LoopInvariant14,LoopInvariant7,LoopInvariant6,LoopInvariant3,LoopInvariant2,Ensures9,Ensures8,H11,Ensures7,Ensures6,H10,Ensures5,Ensures4,H9,H8,Ensures3,Ensures2,Ensures1,Ensures,LoopInvariant1,LoopInvariant,H20,H19,H7,H6,H5,H4,H2,(==)'spec3,(==)'spec2,(==)'spec1,(==)'spec,create'spec1,create'spec,set'spec2,set'spec1,set'spec,singleton'spec1,singleton'spec,cons'spec2,cons'spec1,cons'spec,snoc'spec2,snoc'spec1,snoc'spec,([..])'spec1,([..])'spec,(++)'spec2,(++)'spec1,(++)'spec,Abs_le2,Abs_le1,Abs_le,Div_bound3,Div_bound2,Mod_bound3,Mod_bound2,array63'invariant3,array63'invariant2,array63'invariant1,array63'invariant,Mod_bound1,Mod_bound,Div_bound1,Div_bound,divides'spec1,divides'spec,even_mod21,even_mod2,even_divides1,even_divides,odd_divides1,odd_divides,div_mult_11,div_mult_1,mult_borne_sous_exp1,mult_borne_sous_exp,t'invariant22,t'invariant21,t'invariant20,t'invariant19,t'invariant18,t'invariant17,t'invariant16,t'invariant15,t'invariant14,t'invariant13,t'invariant12,t'invariant11,t'invariant10,t'invariant9,t'invariant8,t'invariant7,t'invariant6,t'invariant5,t'invariant4,t'invariant3,t'invariant2,t'invariant1,t'invariant,Ensures12,Ensures11,Assert4,Assert3,LoopInvariant13,LoopInvariant11,LoopInvariant10,LoopInvariant9,LoopInvariant8,LoopInvariant5,LoopInvariant4,h1
loop invariant preservation---0.020.010.04---0.02
loop invariant preservation---------------0.14
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation------------------
unfold ordered in LoopInvariant7
loop invariant preservation------------------
instantiate LoopInvariant7 i
loop invariant preservation------------------
instantiate Hinst j
loop invariant preservation------------------
case (j = cnt1)
true case (loop invariant preservation)---1.17---0.31------
false case (loop invariant preservation)---0.29---0.27------
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation------------------
unfold all_inf_or_eq in LoopInvariant7
loop invariant preservation------------------
instantiate LoopInvariant7 i
loop invariant preservation------------------
case (i < cnt1)
true case (loop invariant preservation)---0.17---0.27---0.16
false case (loop invariant preservation)---1.33---0.31------
loop invariant preservation---0.22---0.34------
loop invariant preservation------------------
case (i < cnt1)
true case (loop invariant preservation)---0.78---0.33------
false case (loop invariant preservation)---1.13---0.37------
loop invariant preservation------------------
case (i < 2 * p1 + 1)
true case (loop invariant preservation)------------------
instantiate LoopInvariant9 i
true case (loop invariant preservation)---0.64---0.33------
false case (loop invariant preservation)------------------
case (i = 2 * p1 + 1)
false case (true case. loop invariant preservation)---------0.52---0.30
false case (loop invariant preservation)---5.15------------
precondition---0.05---0.25---0.09
postcondition---0.20---0.74------
postcondition---1.22---1.14------
postcondition---0.23---0.29------
postcondition---------0.41------
assertion---0.14------------
assertion---0.18---2.20---0.12
assertion---0.72---0.23------
index in array bounds---0.02---0.21---0.08
loop invariant init---0.03---0.20---0.08
loop invariant init---0.02---0.13---0.02
loop invariant init---0.10---0.23------
loop invariant init---0.02---0.14---0.02
loop invariant init------------------
inline_goal
loop invariant init------------------
split_vc
loop invariant init------------------
assert (forall i. 1 <= i < length (arr t)[0 <- 2] -> (arr t)[i] = (arr t)[0 <- 2][i])
asserted formula---0.04---0.21---0.08
loop invariant init---0.33---0.24---0.08
loop invariant init---0.37---0.24---0.09
loop invariant init---0.13---0.24---0.09
loop invariant init---0.08---0.25---0.09
loop invariant init------------------
assert (forall i. 1 <= i < length (arr t)[0 <- 2] -> (arr t)[i] = (arr t)[0 <- 2][i])
asserted formula---0.06---0.22---0.09
loop invariant init---0.79---0.30---0.12
loop invariant init---0.17---0.32---0.09
loop invariant init---0.04---0.20---0.08
loop invariant init---0.11---0.24---0.08
loop invariant init---0.04---0.26---0.09
loop invariant init---0.11---0.24---0.08
loop invariant init---0.37---0.26---0.12
integer overflow---0.04---0.19---0.08
integer overflow---0.04---0.20---0.08
index in array bounds---0.05---0.22---0.08
division by zero---0.03---0.12---0.02
integer overflow---0.08---0.21------
assertion---0.06---0.22------
index in array bounds---0.05---0.24---0.09
index in array bounds---0.05---0.25---0.10
integer overflow---0.26---0.28---0.10
index in array bounds---0.06---0.24---0.09
index in array bounds---0.07---0.24---0.10
precondition---0.06---0.24---0.10
precondition---0.62---0.32------
assertion------------------
split_vc
assertion------------------
unfold inv_count in LoopInvariant5
assertion------------------
instantiate LoopInvariant5 (int63'int p)
assertion------------------
instantiate LoopInvariant5 (int63'int next)
assertion---------0.33------
assertion------------------
split_vc
assertion---0.62---0.28---0.18
assertion---1.06---0.36------
assertion---0.29---0.28---0.12
precondition---0.03---0.19---0.08
precondition---------3.30---0.14
precondition---1.03---0.39------
precondition---0.08---0.25---0.10
precondition---0.10---0.36------
precondition---0.13---0.42------
assertion---0.33---0.29---0.19
assertion---0.56------------
loop variant decrease---0.08---0.30---0.13
loop invariant preservation---0.04---0.13---0.03
loop invariant preservation---0.04---0.14---0.02
loop invariant preservation---0.04---0.19---0.09
loop invariant preservation---0.04---0.14---0.02
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation------------------
case (i <> p)
true case (loop invariant preservation)---0.92---0.30------
false case (loop invariant preservation)---1.25---0.30---0.51
loop invariant preservation------------------
case (i <> p)
true case (loop invariant preservation)---0.64---0.30---0.20
false case (loop invariant preservation)---0.68---0.28---0.12
loop invariant preservation---1.25---0.28------
loop invariant preservation---0.40---0.30---0.12
loop invariant preservation---0.91---0.38------
loop invariant preservation------------------
case (i <> p)
true case (loop invariant preservation)---8.76------------
false case (loop invariant preservation)---1.45---0.32------
loop invariant preservation---------0.34------
loop invariant preservation---2.15---0.41------
loop invariant preservation---0.24---0.33------
loop invariant preservation---1.05---0.30------
loop invariant preservation---------1.18------
integer overflow---0.05---0.18---0.09
integer overflow---0.05---0.24---0.08
index in array bounds---0.06---0.25---0.09
precondition---0.07---0.24---0.10
precondition---0.04------------
integer overflow---0.06---0.23---0.08
assertion---0.24---0.24---0.11
loop variant decrease---0.41---0.34---0.10
loop invariant preservation---0.21---0.32---0.10
loop invariant preservation---0.27---0.36---0.11
loop invariant preservation---0.09---0.23---0.10
loop invariant preservation---0.07---0.25---0.10
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation---2.52---0.30---0.14
loop invariant preservation---3.41---0.29---0.12
loop invariant preservation---0.44---0.30---0.11
loop invariant preservation---0.34---0.30---0.12
loop invariant preservation------------------
unfold inv_count in LoopInvariant7
loop invariant preservation------------------
split_premise_right
loop invariant preservation------------------
assert (t_arr[cnt1 <- ((2 * p1) + 1)][i] = t_arr[i])
asserted formula---------0.36------
loop invariant preservation------------------
instantiate LoopInvariant9 i
loop invariant preservation------------------
assert (cnt1 <= i < length t_arr1)
asserted formula---0.11---0.23---0.12
loop invariant preservation---5.28------------
loop invariant preservation---------------0.16
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
introduce_premises
loop invariant preservation------------------
split_all_full
loop invariant preservation------------------
case (j = cnt1)
true case (loop invariant preservation)---------0.26------
false case (loop invariant preservation)---0.22---0.41------
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation------------------
unfold all_inf_or_eq in LoopInvariant7
loop invariant preservation------------------
instantiate LoopInvariant7 i
loop invariant preservation------------------
unfold inv_count in LoopInvariant1
loop invariant preservation------------------
split_premise_right
loop invariant preservation------------------
instantiate LoopInvariant6 (int63'int p1)
loop invariant preservation---------0.66------
loop invariant preservation---0.20---0.30------
loop invariant preservation------------------
instantiate LoopInvariant9 i
loop invariant preservation---1.72------------
loop invariant preservation------------------
case (i < 2 * p1 + 1)
true case (loop invariant preservation)------------------
instantiate LoopInvariant9 i
true case (loop invariant preservation)---0.53---0.30------
false case (loop invariant preservation)------------------
case (i = 2 * p1 + 1)
false case (true case. loop invariant preservation)---------0.33---0.29
false case (loop invariant preservation)---2.26------------
integer overflow---0.04---0.19---0.09
integer overflow---0.05---0.24---0.09
index in array bounds---0.06---0.24---0.09
precondition---0.06---0.24---0.08
precondition---0.03---0.28------
integer overflow---0.05---0.26---0.09
integer overflow---0.06---0.24---0.09
assertion---0.16---0.24---0.10
loop variant decrease---0.06---0.26---0.10
loop invariant preservation---0.03---0.18---0.08
loop invariant preservation---0.06---0.24---0.10
loop invariant preservation---0.07---0.25---0.10
loop invariant preservation---0.06---0.25---0.10
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation---------0.30---0.12
loop invariant preservation---1.23---0.32---0.12
loop invariant preservation---0.52---0.30---0.10
loop invariant preservation---0.28---0.30---0.11
loop invariant preservation------------------
unfold inv_count in LoopInvariant7
loop invariant preservation------------------
split_premise_right
loop invariant preservation------------------
assert (t_arr[cnt1 <- ((2 * p1) + 1)][i] = t_arr[i])
asserted formula---------0.37------
loop invariant preservation------------------
instantiate LoopInvariant9 i
loop invariant preservation------------------
assert (cnt1 <= i < length t_arr1)
asserted formula---0.10---0.23---0.12
loop invariant preservation------1.90---------
remove zero1,one1,(-),(>),(<=),(>=),abs,int63'maxInt,int63'minInt,min_int63,max_int63,to_int,in_bounds,zero,one,even,odd,divides,prime,([]),singleton,cons,snoc,(++),exchange,inv_nexts,all_eliminated_marked,all_eliminated_marked_partial,not_marked_impl_next_not_marked,is_copy,not_marked_impl_next_not_marked_partial,all_primes,all_multiples_marked,previously_marked_multiples,only_multiples_marked,prime_multiples_marked,inv_remove_products,ordered,all_inf_or_eq,inv_count,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_pos,Div_mod,Div_unique,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_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,to_int_in_bounds,extensionality,max_int'def,min_int'def,even_or_odd,even_not_odd,odd_not_even,even_odd,odd_even,even_even,odd_odd,even_2k,odd_2k1,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,not_prime_1,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,mult_croissance_locale,mult_croissance,comp_mult_2,div_croissance_locale1,div_croissance1,div_croissance_locale2,div_croissance2,sq_ineq,divides_div,divides_inf,not_prime_divider_limits,no_prod_impl_no_divider,not_prime_impl_divisor_under_sqrt,length_nonnegative,empty'def,set'def,([<-])'def,([..])'def,([_..])'def,([.._])'def,exchange_set,conservation_all_eliminated_marked_on_marked_change,conservation_all_eliminated_marked_on_nexts_change,conservation_inv_arr_on_mark,conservation_inv_arr_on_jump,multiples_of_marked_are_marked,prev_and_new_impl_all_multiples_marked,conservation_only_multiples_marked,conservation_previously_marked_multiples,conservation_previously_marked_multiples_on_marked_change,conservation_not_marked_impl_next_not_marked,unchanged_other_elements,previously_marked_multiples_impl_prime,only_multiples_marked_impl_not_marked,H24,H23,Ensures16,Ensures15,Ensures14,Ensures13,H22,H21,Assert2,Assert1,H18,H17,Ensures10,H16,H15,H14,H13,H12,LoopInvariant15,LoopInvariant14,LoopInvariant7,LoopInvariant6,LoopInvariant3,LoopInvariant2,Ensures9,Ensures8,H11,Ensures7,Ensures6,H10,Ensures5,Ensures4,H9,H8,Ensures3,Ensures2,Ensures1,Ensures,LoopInvariant1,LoopInvariant,H20,H19,H7,H6,H5,H4,H2,(==)'spec3,(==)'spec2,(==)'spec1,(==)'spec,create'spec1,create'spec,set'spec2,set'spec1,set'spec,singleton'spec1,singleton'spec,cons'spec2,cons'spec1,cons'spec,snoc'spec2,snoc'spec1,snoc'spec,([..])'spec1,([..])'spec,(++)'spec2,(++)'spec1,(++)'spec,Abs_le2,Abs_le1,Abs_le,Div_bound3,Div_bound2,Mod_bound3,Mod_bound2,array63'invariant3,array63'invariant2,array63'invariant1,array63'invariant,Mod_bound1,Mod_bound,Div_bound1,Div_bound,divides'spec1,divides'spec,even_mod21,even_mod2,even_divides1,even_divides,odd_divides1,odd_divides,div_mult_11,div_mult_1,mult_borne_sous_exp1,mult_borne_sous_exp,t'invariant22,t'invariant21,t'invariant20,t'invariant19,t'invariant18,t'invariant17,t'invariant16,t'invariant15,t'invariant14,t'invariant13,t'invariant12,t'invariant11,t'invariant10,t'invariant9,t'invariant8,t'invariant7,t'invariant6,t'invariant5,t'invariant4,t'invariant3,t'invariant2,t'invariant1,t'invariant,Ensures12,Ensures11,Assert4,Assert3,LoopInvariant13,LoopInvariant11,LoopInvariant10,LoopInvariant9,LoopInvariant8,LoopInvariant5,LoopInvariant4,h1
loop invariant preservation---0.020.010.03---0.02
loop invariant preservation---------------0.14
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation------------------
unfold ordered in LoopInvariant7
loop invariant preservation------------------
instantiate LoopInvariant7 i
loop invariant preservation------------------
instantiate Hinst j
loop invariant preservation------------------
case (j = cnt1)
true case (loop invariant preservation)---1.88---0.28------
false case (loop invariant preservation)---0.14---0.26------
loop invariant preservation------------------
inline_goal
loop invariant preservation------------------
split_vc
loop invariant preservation------------------
unfold all_inf_or_eq in LoopInvariant7
loop invariant preservation------------------
instantiate LoopInvariant7 i
loop invariant preservation------------------
case (i < cnt1)
true case (loop invariant preservation)---0.13---0.26---0.14
false case (loop invariant preservation)---0.71---0.30------
loop invariant preservation---0.18---0.32------
loop invariant preservation---2.47---0.50------
loop invariant preservation------------------
case (i < 2 * p1 + 1)
true case (loop invariant preservation)------------------
instantiate LoopInvariant9 i
true case (loop invariant preservation)---0.77---0.32------
false case (loop invariant preservation)------------------
case (i = 2 * p1 + 1)
false case (true case. loop invariant preservation)---------0.46---0.27
false case (loop invariant preservation)---2.86------------
precondition---0.04---0.21---0.08
postcondition---0.21---0.68------
postcondition---1.13---0.88------
postcondition---0.22---0.28------
postcondition---------0.72------