Find loop invariant of this function

Question

I need to find the loop invariant of gcd (euclid algorithm) but i don't know from where to start or what to look

    int f(int x, int y) {
       while (true) {
           int m = x % y;
           if(m == 0) return y;
           x = y;
           y = m;
       }
    }

Answer 1

The greatest common divisor of x and y remains the same throughout the loop. Therefore, a loop invariant is gcd(x,y) = c where c is a constant.

Answer 2

A loop invariant is a condition that is met in every iteration of the loop. In your case, you're not looping on a condition that can change, so if the loop invariant isn't "the loop condition is always true", the only other thing that holds true for every iteration is "the value of m always shows whether x can be divided by y".