From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sun, 30 Apr 2017 16:25:24 +0000 (+0200)
Subject: corrected invariant of sieve
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=0e27c680820b69389067a390661c3b5cc72660be;p=cfuerst%2Fformal-numbers.git

corrected invariant of sieve
---

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
index e410057..e30f59d 100644
--- a/sieveEratosthenes.txt
+++ b/sieveEratosthenes.txt
@@ -35,9 +35,11 @@ proc SieveOfErathostenes(m:nat): Array[MAX,Bool]
 
    for var i:nat=2; i ≤ rootOfp; i=i+1 do
       invariant 2 ≤ i ∧ i ≤ rootOfp+2;
-      invariant ∀j:nat with j < i. (ret[j] = true)  ⇔ (isPrime(j) ∧
-                                                      (∀l:nat with j < l. (divides(j,l) ⇒ ¬isPrime(l))));
+      // Prime elements in range 2..rootOfp
+      invariant ∀j:nat with j < i. (ret[j] = true)  ⇔ isPrime(j);
       invariant ∀j:nat with j < i. (ret[j] = false) ⇔ ¬isPrime(j);
+      // Prime divisors that have already been processed
+      invariant ∀j:nat with 2 < i ∧ i < j ∧ j < MAX. ( divides(i-1,j) ⇒ ret[j] = false);
       decreases rootOfp+2-i;
    {
         if ret[i] = true then
@@ -46,6 +48,7 @@ proc SieveOfErathostenes(m:nat): Array[MAX,Bool]
                invariant 1 ≤ k ∧ k ≤ MAX/i;
                invariant ∀p:nat with p ≤ i. (ret[p] = true ⇒
                     //  p+r*i < MAX is implied by range of k
+                    // partial processed array
                    (∀r:nat with 1 ≤ r ∧ r < k. ret[(r+1)*p] = false));
                decreases MAX/i - k;
             {
@@ -102,3 +105,4 @@ proc SieveOfErathostenesSet(m:nat): Set[nat]
    return ret;
 }
 
+