查找此函数的循环不变式

问题描述

我需要找到gcd的循环不变式（欧几里得算法），但我不知道从哪里开始或看上去是什么

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

解决方法

x和y的最大公约数在整个循环中保持相同。因此，循环不变性为gcd（x，y）= c，其中c为常数。

,

循环不变性是循环的每次迭代都满足的条件。在您的情况下，您不会在可能发生变化的条件上循环，因此，如果循环不变式不是“循环条件始终为真”，则每次迭代唯一适用的另一件事是“ m的值始终显示x是否可以除以y”。