java - 求该函数的循环不变量

Question

我需要找到 gcd(欧几里德算法)的循环不变式，但我不知道从哪里开始或看什么

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

Answer 1

x 和 y 的最大公约数在整个循环中保持不变。因此，循环不变量是 gcd(x,y) = c，其中 c 是常数。