// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // The following module implements the extended Euclidean algorithm: Given two// // integers a and b, the algorithm computes a triple (u,v,g) such that // // u*a + v*b = gcd(a,b). The computation is based on the constructive proof // // of the Lemma of Bézout. The core of the algorithm is however Euclid's // // algorithm which in turn is based on the fact that the common divisors of a // // and b are the common divisors of b and (a%b): // // * Divisors(a,b) <= Divisors(b,a%b) holds, since x*t=a, y*t=b, and a=q*b+r // // imply x*t = q*y*t+r, i.e., r = (x-q*y) * t so that each common divisor t// // of a and b also divides r = a%b. // // * Divisors(b,a%b) <= Divisors(a,b) holds, since x*t=b, y*t=r, and a=q*b+r // // imply a = q*x*t+y*t = (q*x+y)*t, so that each common divisor t // // of b and r=a%b also divides a. // // Thus, gcd(a,b) = gcd(b,a%b) which is the recursive step of the Euclidean // // algorithm. The invariants maintained in the algorithm shown below are due // // to Bézout's Lemma and moreover compute the numbers u and v. // // ************************************************************************** // module ExtEuclid(int ?a,?b,u,v,g,event !rdy) { int m,n,q,s,t; m = a; n = b; u = 1; v = 0; s = 0; t = 1; assert(m == u*a + v*b); assert(n == s*a + t*b); // The loop maintains the following invariants: // (1) m == u*a + v*b // (2) n == s*a + t*b // (3) gcd(m,n) = gcd(a,b) // Note that (3) is invariant since gcd(m,n) = gcd(n,m%n), and the other // invariants are immediately seen by expanding the assignments. while(n!=0) { q = m / n; next(m) = n; next(n) = m - q * n; next(u) = s; next(v) = t; next(s) = u - q * s; next(t) = v - q * t; pause; assert(m == u*a + v*b); assert(n == s*a + t*b); } // since n=0 holds, we conclude the following from the invariants // (1) m == u*a + v*b // (2) 0 == s*a + t*b // (3) gcd(m,0) = m = gcd(a,b) g = m; emit(rdy); } drivenby { a = 99; b = 78; immediate await(rdy); assert(u*a+v*b==g); assert(a%g==0 & b%g==0); } drivenby { a = 683; b = 147; immediate await(rdy); assert(u*a+v*b==g); assert(a%g==0 & b%g==0); }