From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sun, 21 May 2017 18:45:01 +0000 (+0200)
Subject: added invariants
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=af94eb808ac2e541cc664b13b575a14e35e1e0f8;p=cfuerst%2Fformal-numbers.git

added invariants
---

diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt
index e30f59d..2449a5a 100644
--- a/sieveEratosthenes.txt
+++ b/sieveEratosthenes.txt
@@ -46,6 +46,8 @@ proc SieveOfErathostenes(m:nat): Array[MAX,Bool]
         {
             for var k:nat=1;i*(k+1)<MAX;k=k+1 do
                invariant 1 ≤ k ∧ k ≤ MAX/i;
+               invariant ∀j:nat with j < i. (ret[j] = true)  ⇔ isPrime(j);
+               invariant ∀j:nat with j < i. (ret[j] = false) ⇔ ¬isPrime(j);
                invariant ∀p:nat with p ≤ i. (ret[p] = true ⇒
                     //  p+r*i < MAX is implied by range of k
                     // partial processed array