Мне нужно найти инвариант цикла 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 можно разделить на у.
