Corrected Loop invariant of quadratic residue

diff --git a/numbertheory.txt b/numbertheory.txt
index 5931103..db634d8 100644 (file)
--- a/numbertheory.txt
+++ b/numbertheory.txt
@@ -62,35 +62,43 @@ proc isprime(p:nat): Bool
 }
 
 
+////////////////////////////////////////////////////////////////////
 // Quadratic residue
 // a ∈ ℤ/pℤ is a quadratic residue ⇔
 // 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;
+   var i:nat = 1;
    if isprime(p) then
    {
-      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 a%p = 0 then
+         res = true;
+      else
       {
-         if (i^2-a)%p = 0 then
-            res = true;
-         i = i+1;
+         while i < p ∧ res = false do
+            invariant (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;
 }
 
+////////////////////////////////////////////////////////////////////
 // Legendre Symbol   (a/p)
 // ==  0   divides(p,a)
 // ==  1   a is quadratic residue modulo p
 // == -1   a is NOT quadratic residue modulo p
+////////////////////////////////////////////////////////////////////
 
 
 ////////////////////////////////////////////////////////////////////
@@ -136,3 +144,4 @@ proc xpowern(x:Base,n:Exp): Result
 
 
 
+