Precondition: x, y ? N, x, y > 0
Postcondition: return an integer representing the greatest common divisor of x and y
euclidGCD(x, y):
while(y != 0):
temp = y
y = x % y
x = temp
return x
Prove the correctness of this iterative program.
In the proof can you write down the loop invariant, how the loop terminates and how the loop invariant holds after the exit condition?