From af94eb808ac2e541cc664b13b575a14e35e1e0f8 Mon Sep 17 00:00:00 2001
From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sun, 21 May 2017 20:45:01 +0200
Subject: [PATCH] added invariants

---
 sieveEratosthenes.txt | 2 ++
 1 file changed, 2 insertions(+)

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
-- 
2.1.4