From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Tue, 21 Mar 2017 18:46:09 +0000 (+0100)
Subject: Added definition of quadratic residue. TODO: It is defined for primes only, consider... 
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=da07e4a300f1ff470ce5ceda48a6a2a4e29dea8d;p=cfuerst%2Fformal-numbers.git

Added definition of quadratic residue. TODO: It is defined for primes only, consider in definition. Define Postcondition
---

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(): ()
 
 
 
+