可以描述此代码功能的循环不变性/不变量是什么？

Question

def func(no_1,no_2):
    a=no_1
    b=no_2
    while(b):
        a,b=b,a%b
    return a

其中 no_1 和 no_2 是正实数

我发现这个函数返回 no_1 和 no_2 的最大公因数。首先，我尝试了 (no_1%a 和 no_2%a) ≥ 0 的循环不变性，使得 a、no_1 和 no_2 是正整数，但在终止时，我只能证明 no_1%a = 0 = no_2%a，即根本没有描述功能。那么谁能告诉我这个函数有什么可能的循环不变性来描述它的功能？

Answer 1

下面我假设no_1 和no_2 都是一些自然数。

我认为您可以尝试引入一个额外的符号 fact，它不确定地分配给 no_1 和 no_2 的某些公因子：假设 no_1 % fact == 0 and no_2 % fact == 0。

然后作为循环不变量，您可以声明a >= fact。