python - 找到该幂函数的循环不变量

Question

在我的计算理论类(class)中，我很难掌握证明迭代程序/函数正确性的概念。更具体地说，我不知道如何提出循环不变量。我知道一个函数可以有多个循环不变量，但如何找到一个可以帮助我们证明后置条件的变量对我来说完全是个谜。我目前正在做一些作业，不知道如何找到以下函数的循环不变式。

PREcondition: a is a number, b is a natural number.
POSTcondition: return a^b.
    def power(a, b):
        s = a
        k = b
        p = 1
        while k > 0:
            if k % 2 == 1:
                p = p * s
            s = s * s
            k = k // 2
        return p

到目前为止，我了解该函数是如何工作的，但正如我之前所说，当我试图找到一个合适的循环不变量来帮助我证明该函数返回 a^b 时，我非常迷失。

Answer 1

请注意，虽然 ^ 在某些语言中表示“幂”，但在 Python 中它是按位异或。幂运算符是 **

这里有一些检查循环是否朝着正确的结果前进

    while k > 0:
        assert s ** k * p == a ** b
        if k % 2 == 1:
            p = p * s
        s = s * s
        k = k // 2
        assert k == 0 or s ** k * p == a ** b

也可以编写防御性不变量，例如

s >= a
n <= b