formulated invariant for sieveOfErathostenes

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
index cc7b6aa..e410057 100644 (file)
--- a/sieveEratosthenes.txt
+++ b/sieveEratosthenes.txt
@@ -13,7 +13,9 @@ proc IntegerRoot(a:nat): nat
    var z:ℕ[(MAX+1)^2] = 1;
 
    while y ≤ a do
-      invariant x^2 ≤ a ∧ y = x^2+z ∧ z = 2*x+1;
+      invariant 1 ≤ y ∧ y = x^2+z;
+      invariant 0 ≤ x ∧ x^2 ≤ a;
+      invariant 1 ≤ z ∧ z = 2*x+1;
       decreases a-x^2;
    {
       x=x+1;
@@ -28,19 +30,26 @@ proc SieveOfErathostenes(m:nat): Array[MAX,Bool]
    ensures ∀p:nat with p < m. (result[p]=true ⇔ isPrime(p));
 {
    var ret:Array[MAX,Bool] := Array[MAX,Bool](true);
+   var rootOfp:nat = IntegerRoot(m);
    ret[0] = false; ret[1] = false;
 
-   for var i:nat=2; i≤IntegerRoot(m); i=i+1 do
-      invariant (ret[i] = true) ∨ (∃j:nat. 1 < j ∧ j < i ∧ divides(j,i));
-      decreases IntegerRoot(m)+2-i;
+   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))));
+      invariant ∀j:nat with j < i. (ret[j] = false) ⇔ ¬isPrime(j);
+      decreases rootOfp+2-i;
    {
         if ret[i] = true then
         {
-            for var k:nat=0;i^2+k*i<MAX;k=k+1 do
-               invariant ∀l:nat. (l<k ∧ i^2+l*i < MAX) ⇒ (ret[i^2+l*i] = false);
-               decreases MAX+2 - (i^2 + k*i);
+            for var k:nat=1;i*(k+1)<MAX;k=k+1 do
+               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
+                   (∀r:nat with 1 ≤ r ∧ r < k. ret[(r+1)*p] = false));
+               decreases MAX/i - k;
             {
-                ret[i^2+k*i] = false;
+                ret[i*(k+1)] = false;
             }
         }
    }
@@ -68,9 +77,10 @@ proc SetMin(s:Set[nat]): nat
 fun SetMin2(s:Set[nat]): nat
     requires s ≠ ∅[nat];
     ensures result ∈ s ∧ ∀e ∈ s. result ≤ e;
- = choose m in s with ∀e in s. m <= e;
+ = choose m in s with ∀e in s. m ≤ e;
 
-theorem PrimeDivisor() ⇔ ∀e:nat. (e > 1 ∧ ¬isPrime(e)) ⇒ ∃p:nat. p<e ∧ isPrime(p) ∧ e%p = 0;
+theorem PrimeDivisor()   ⇔ ∀e:nat. (e > 1 ∧ ¬isPrime(e)) ⇒ ∃p:nat. p<e ∧ isPrime(p) ∧ e%p = 0;
+theorem MinOfSetExists() ⇔ ∀s:Set[nat] with s ≠ ∅[nat]. ∃e:nat. 0 ≤ e ∧ e ≤ MAX ∧ e ∈ s ∧ ∀m ∈ s. e ≤ m;
 
 proc SieveOfErathostenesSet(m:nat): Set[nat]
    ensures ∀e:nat. e ≤ m ⇒ (e ∈ result ⇔ isPrime(e));
@@ -92,7 +102,3 @@ proc SieveOfErathostenesSet(m:nat): Set[nat]
    return ret;
 }
 
-
-
-
-