From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Wed, 22 Mar 2017 17:26:21 +0000 (+0100)
Subject: Tried to formulate loop invariant for quadraticresidue - NOT YET WORKING
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=6b8599338015b238db5471d60d4840656a8599e0;p=cfuerst%2Fformal-numbers.git

Tried to formulate loop invariant for quadraticresidue - NOT YET WORKING
---

diff --git a/numbertheory.txt b/numbertheory.txt
index 60c3d5d..5931103 100644
--- a/numbertheory.txt
+++ b/numbertheory.txt
@@ -67,15 +67,21 @@ proc isprime(p:nat): Bool
 // x^2 - a has a zero in ℤ/pℤ
 // defined for p prime > 2 only
 proc isquadraticresidue(a:nat,p:nat): Bool
+   ensures result ⇒ (∃i:nat. 0 ≤ i ∧ i < p ∧ (i^2 - a)%p = 0);
 {
    var res:Bool = false;
    var i:nat = 0;
-
-   while i < p ∧ res = false do
+   if isprime(p) then
    {
-      if (i^2-a)%p = 0 then
-         res = true;
-      i = i+1;
+      while i < p ∧ res = false do
+         invariant ((~res) ∧ ((i = 0) ∨ (∀j:nat. 0 ≤ j ∧ j ≤ i ∧ (j^2 - a)%p ≠ 0))) ∨
+                    ((res) ∧ (∃j:nat. 0 ≤ j ∧ j ≤ i ∧ (j^2 - a)%p = 0));
+         decreases p-i;
+      {
+         if (i^2-a)%p = 0 then
+            res = true;
+         i = i+1;
+      }
    }
 
    return res;
@@ -88,7 +94,7 @@ proc isquadraticresidue(a:nat,p:nat): Bool
 
 
 ////////////////////////////////////////////////////////////////////
-// Algorithm: Calcluate x^n by Right-To-Left Exponentation
+// Algorithm: Calculate x^n by Right-To-Left Exponentation
 ////////////////////////////////////////////////////////////////////
 proc r2lexponentation(x:Base,n:Exp): Result
    ensures result = x^n;
@@ -129,3 +135,4 @@ proc xpowern(x:Base,n:Exp): Result
 }
 
 
+