added invariants

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
index e30f59d..2449a5a 100644 (file)
--- a/sieveEratosthenes.txt
+++ b/sieveEratosthenes.txt
@@ -46,6 +46,8 @@ proc SieveOfErathostenes(m:nat): Array[MAX,Bool]
         {
             for var k:nat=1;i*(k+1)<MAX;k=k+1 do
                invariant 1 ≤ k ∧ k ≤ MAX/i;
+               invariant ∀j:nat with j < i. (ret[j] = true)  ⇔ isPrime(j);
+               invariant ∀j:nat with j < i. (ret[j] = false) ⇔ ¬isPrime(j);
                invariant ∀p:nat with p ≤ i. (ret[p] = true ⇒
                     //  p+r*i < MAX is implied by range of k
                     // partial processed array