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

问题描述

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 and no_2%a) ≥ 0 的循环不变性，使得 a、no_1 和 no_2 是正整数，但在终止时，我只能证明 no_1%a = 0 = no_2%a，其中根本不描述功能。那么谁能告诉我这个函数有什么可能的循环不变性来描述它的功能？

解决方法

在下文中，我假设 no_1 和 no_2 都是一些自然数。

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

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