查找此函数的循环不变量

【问题标题】：Find loop invariant of this function查找此函数的循环不变量
【发布时间】：2020-08-30 20:40:21
【问题描述】：

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

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

【问题讨论】：

你的代码不是 loop invariant 了吗？它永远是true。

标签： java algorithm loop-invariant

【解决方案1】：

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

【讨论】：

x > y 仅当您忽略第一次循环迭代时才是不变量，其中它不一定成立。

【解决方案2】：

循环不变量是在循环的每次迭代中都满足的条件。在您的情况下，您不是在可以更改的条件上循环，因此如果循环不变量不是“循环条件始终为真”，那么每次迭代都适用的唯一另一件事是“m 的值始终显示 x 是否可以除以 y"。

【讨论】：