java - 查找此函数的循环不变量

Question

我需要找到 gcd（euclid 算法）的循环不变量，但我不知道从哪里开始或看什么

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

标签： javaalgorithmloop-invariant

Answer 1

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