From 566af1a548c3267c32ef53c15db7d7268aae1c14 Mon Sep 17 00:00:00 2001
From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Tue, 11 Apr 2017 20:39:22 +0200
Subject: [PATCH] Implemented Set-Based View on Sieve Of Erathostenes

---
 sieveEratosthenes.txt | 69 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)
 create mode 100644 sieveEratosthenes.txt

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
new file mode 100644
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);
+}
+
+
-- 
2.1.4