From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Thu, 20 Apr 2017 15:34:44 +0000 (+0200)
Subject: corrected wrong last invariant in sieveSet
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=830d7187fd8650b958726bb34d3a7f54e2e965fe;p=cfuerst%2Fformal-numbers.git

corrected wrong last invariant in sieveSet
---

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
index a26805b..cc7b6aa 100644
--- a/sieveEratosthenes.txt
+++ b/sieveEratosthenes.txt
@@ -83,7 +83,7 @@ proc SieveOfErathostenesSet(m:nat): Set[nat]
       invariant start ⊆ 2..m ∧ ret ⊆ 2..m;
       invariant ∀e ∈ ret. isPrime(e);
       invariant start ≠ ∅[nat] ⇒ ∀e ∈ ret. e < SetMin(start);
-      invariant ∀e:nat. e ≤ m ∧ e ∈ start ⇒ ¬ (e ∈ ret);
+      invariant ∀e:nat. e ≤ m ∧ ¬(e ∈ start) ∧ isPrime(e) ⇒ e ∈ ret;
    {
       var locmi:nat = SetMin(start);
       ret = ret ∪ {locmi};
@@ -95,3 +95,4 @@ proc SieveOfErathostenesSet(m:nat): Set[nat]
 
 
 
+