From da07e4a300f1ff470ce5ceda48a6a2a4e29dea8d Mon Sep 17 00:00:00 2001 From: Christoph Fuerst Date: Tue, 21 Mar 2017 19:46:09 +0100 Subject: [PATCH] Added definition of quadratic residue. TODO: It is defined for primes only, consider in definition. Define Postcondition --- numbertheory.txt | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/numbertheory.txt b/numbertheory.txt index 23db6de..db521a3 100644 --- a/numbertheory.txt +++ b/numbertheory.txt @@ -9,6 +9,34 @@ type Exp = ℕ[M]; type Result = ℕ[N^M]; type nat = ℕ[K]; +// Elementary division +pred divides(m:nat,n:nat) ⇔ ∃p:nat. m*p = n; + +// 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 +{ + var res:Bool = false; + var i:nat = 0; + + while i < p ∧ res = false do + { + 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 + + //////////////////////////////////////////////////////////////////// // Algorithm: Calcluate Integer Root of a // See http://www.inf.fh-flensburg.de/lang/se/veri/aufg/wurzel.htm @@ -97,3 +125,4 @@ proc main(): () + -- 2.1.4