From 852f38da87425b1bbb42279e54433d4ddb5fbfaf Mon Sep 17 00:00:00 2001 From: Christoph Fuerst Date: Thu, 23 Mar 2017 20:28:58 +0100 Subject: [PATCH] Initial introduction of Legendre Symbol --- numbertheory.txt | 31 ++++++++++++++++++++++++++----- 1 file changed, 26 insertions(+), 5 deletions(-) diff --git a/numbertheory.txt b/numbertheory.txt index db634d8..11702c3 100644 --- a/numbertheory.txt +++ b/numbertheory.txt @@ -4,10 +4,11 @@ val N: ℕ; val M: ℕ; val K: ℕ; -type Base = ℕ[N]; -type Exp = ℕ[M]; -type Result = ℕ[N^M]; -type nat = ℕ[K]; +type Base = ℕ[N]; +type Exp = ℕ[M]; +type Result = ℕ[N^M]; +type nat = ℕ[K]; +type integer = ℤ[-K,K]; // Elementary division pred divides(m:nat,n:nat) ⇔ ∃p:nat. m*p = n; @@ -98,8 +99,28 @@ proc isquadraticresidue(a:nat,p:nat): Bool // == 0 divides(p,a) // == 1 a is quadratic residue modulo p // == -1 a is NOT quadratic residue modulo p +// == 2 if p is not prime //////////////////////////////////////////////////////////////////// +proc legendre(a:nat,p:nat): integer + ensures (((result = 0) ∧ divides(p,a)) ∨ + ((result = 1) ∧ isquadraticresidue(p,a)) ∨ + ((result = -1) ∧ ~isquadraticresidue(p,a)) ∨ + ((result = 2) ∧ ~isprime(p))); +{ + var res:integer = 0; + if isprime(p) then + if divides(p,a) then + res = 0; + else if isquadraticresidue(p,a) then + res = 1; + else + res = -1; + else + res = 2; + + return res; +} //////////////////////////////////////////////////////////////////// // Algorithm: Calculate x^n by Right-To-Left Exponentation @@ -131,7 +152,7 @@ proc xpowern(x:Base,n:Exp): Result ensures result = x^n; { var res:Result = 1; - var i:Nat[M+1] = 0; + var i:ℕ[M+1] = 0; while i < n do invariant 0 ≤ i ∧ i ≤ n ∧ res = x^i; decreases n-i+1; -- 2.1.4