From 13658c99fda83834740d2eceec9bb39cf603ab79 Mon Sep 17 00:00:00 2001 From: Christoph Fuerst Date: Thu, 23 Mar 2017 20:18:11 +0100 Subject: [PATCH] Corrected Loop invariant of quadratic residue --- numbertheory.txt | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/numbertheory.txt b/numbertheory.txt index 5931103..db634d8 100644 --- 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 + -- 2.1.4