The greatest common divisor (GCD) of two integers a and b is defined as the largest integer that can divide both a and b without a remainder. For example, the GCD of 30 and 54 is 6, whereas the GCD of 7 and 5 is 1. The following procedure was developed by Euclid to compute the greatest common divisor of two positive integers a and b. In this exercise, we will prove the correctness of this algorithm. procedure Euclidean(a, b) 1 x ← a 2 y ← b 3 while x 6= y do 4 if x > y then 5 x ← x − y 6 else 7 y ← y − x 8 return x (a) State the loop invariant for the while loop in this procedure.
(b) Prove the loop invariant.
(c) Prove that procedure Euclidean always terminates provided that a and b are positive integers.
(d) Using the termination property of your loop invariant, prove that procedure Euclidean computes and returns the greatest common divisor of a and b.