From 0e27c680820b69389067a390661c3b5cc72660be Mon Sep 17 00:00:00 2001 From: Christoph Fuerst Date: Sun, 30 Apr 2017 18:25:24 +0200 Subject: [PATCH] corrected invariant of sieve --- sieveEratosthenes.txt | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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; } + -- 2.1.4