From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Wed, 19 Apr 2017 20:07:01 +0000 (+0200)
Subject: Updates after Review Wolfgang
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=ba61150cd095c4b977c51bda62c24b2cc69a19f5;p=cfuerst%2Fformal-numbers.git

Updates after Review Wolfgang
---

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
index 11a16ce..6b27a8a 100644
--- a/sieveEratosthenes.txt
+++ b/sieveEratosthenes.txt
@@ -3,8 +3,7 @@ val MAX: ℕ;
 type nat = ℕ[MAX];
 
 pred divides(m:nat,n:nat) ⇔ ∃p:nat. m⋅p = n;
-pred isPrime(m:nat) ⇔ (m = 0) ∨ (m=1) ∨
-                      (1 < m ∧ ∀n:nat. divides(n,m) ⇒ (n≤1 ∨ n=m));
+pred isPrime(m:nat) ⇔ m > 1 ∧ ∀n:nat. n>1 ∧ divides(n,m) ⇒ (n = m);
 
 proc IntegerRoot(a:nat): nat
    ensures result^2 ≤ a ∧ a < (result+1)^2;
@@ -25,34 +24,33 @@ proc IntegerRoot(a:nat): nat
 
 
 proc SieveOfErathostenes(m:nat): Array[MAX,Bool]
-   requires m>1;
-   ensures ∀p:nat. ((p < m ∧ result[p]=true) ⇒ isPrime(p));
+   ensures ∀p:nat with p < m. (result[p]=true ⇔ isPrime(p));
 {
    var ret:Array[MAX,Bool] := Array[MAX,Bool](true);
-   var i:nat;
-   var k:nat = 0;
-   var j:nat;
+   ret[0] = false; ret[1] = false;
 
-   for i=2; i≤IntegerRoot(m); i=i+1 do
-      decreases IntegerRoot(m)+1-i;
+   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;
    {
         if ret[i] = true then
         {
-            for k=0;i^2+k*i<MAX;k=k+1 do
+            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);
             {
-                j=i^2+k*i;
-                ret[j] = false;
+                ret[i^2+k*i] = false;
             }
         }
    }
    return ret;
 }
 
-proc SetMin(s:Set[ℕ[MAX]]): ℕ[MAX]
-   requires s ≠ ∅[ℕ[MAX]];
-   ensures ∀e ∈ s. result ≤ e;
+proc SetMin(s:Set[nat]): nat
+   requires s ≠ ∅[nat];
+   ensures result ∈ s ∧ ∀e ∈ s. result ≤ e;
 {
-   var ret:ℕ[MAX] := MAX;
+   var ret:nat := MAX;
 
    for x in s do
    {
@@ -64,21 +62,25 @@ proc SetMin(s:Set[ℕ[MAX]]): ℕ[MAX]
    return ret;
 }
 
-proc SieveOfErathostenesSet(m:ℕ[MAX]): Set[ℕ[MAX]]
-   requires m>1;
-   ensures ∀e ∈ result. isPrime(e);
+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;
+
+proc SieveOfErathostenesSet(m:nat): Set[nat]
+   ensures ∀e:nat. e ≤ m ⇒ (e ∈ result ⇔ isPrime(e));
 {
-   var start:Set[ℕ[MAX]] := 2..m;
-   var ret:Set[ℕ[MAX]]   := ∅[ℕ[MAX]];
-   var locmi:ℕ[MAX];
+   var start:Set[nat] := 2..m;
+   var ret:Set[nat]   := ∅[nat]; 
 
-   while start ≠ ∅[ℕ[MAX]] do
-      invariant ∀e ∈ ret. isPrime(e);
+   while start ≠ ∅[nat] do
+      invariant ret ⊆ 2..m ∧ ∀e ∈ ret. isPrime(e);
    {
-      locmi = SetMin(start);
+      var locmi:nat = SetMin(start);
       ret = ret ∪ {locmi};
       start = start \ ({locmi} ∪ { if divides(locmi,x) then x else locmi | x ∈ start});
    }
    return ret;
 }
 
+