From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Tue, 11 Apr 2017 18:39:22 +0000 (+0200)
Subject: Implemented Set-Based View on Sieve Of Erathostenes
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=566af1a548c3267c32ef53c15db7d7268aae1c14;p=cfuerst%2Fformal-numbers.git

Implemented Set-Based View on Sieve Of Erathostenes
---

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);
+}
+
+