Implemented Set-Based View on Sieve Of Erathostenes

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
new file mode 100644 (file)
index 0000000..77b5d46
--- /dev/null
+++ b/sieveEratosthenes.txt
@@ -0,0 +1,69 @@
+
+val MAX: ℕ;
+
+type nat = ℕ[MAX];
+
+pred divides(m:nat,n:nat) ⇔ ∃p:nat. m⋅p = n;
+pred isPrime(m:nat) ⇔ 1 < m ∧ ∀n:nat. divides(n,m) ⇒ (n≤1 ∨ n=m);
+
+proc SieveOfErathostenes(m:ℕ[MAX]): Array[MAX,nat]
+   requires m>1;
+   ensures ∀p:ℕ[MAX]. result[p]=1 ⇒ isPrime(p+1);
+{
+   var ret:Array[MAX,nat] := Array[MAX,nat](0);
+   var i:ℕ[MAX];
+   var j:ℕ[2*MAX];   
+   
+   ret[0] = 1;
+   ret[1] = 1;
+   
+//   for i=2;i<N;i=i+1 do
+   {
+//      if ret[i-1] = 1 then
+      {
+         ret[i-1] = 1;
+         for j=(i-1)^2;j<MAX;j=j+i do
+            ret[j] = 1;
+      }
+      print ret;
+   }
+
+   return ret;
+}
+
+proc SetMin(s:Set[ℕ[MAX]]): ℕ[MAX]
+   requires s ≠ ∅[ℕ[MAX]];
+   ensures ∀e ∈ s. result ≤ e;
+{
+   var ret:ℕ[MAX] := MAX;
+   
+   for x in s do
+     if x < ret then
+        ret = x;
+   
+   return ret;
+}
+
+proc SieveOfErathostenesSet(m:ℕ[MAX]): Set[ℕ[MAX]]
+   requires m>1;
+   ensures ∀e ∈ result. isPrime(e);
+{
+   var start:Set[ℕ[MAX]] := 2..m;
+   var ret:Set[ℕ[MAX]]   := ∅[ℕ[MAX]];
+   var locmi:ℕ[MAX];
+
+   while start ≠ ∅[ℕ[MAX]] do
+   {
+      locmi = SetMin(start);
+         ret = ret ∪ {locmi};
+         start = start \ ({locmi} ∪ { if divides(locmi,x) then x else locmi | x ∈ start});
+   }  
+   return ret;
+}
+
+proc main(): ()
+{
+   SieveOfErathostenesSet(MAX);
+}
+
+