1

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

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 时，我非常迷茫。

4

1 回答 1

2

请注意，虽然^在某些语言中意味着“权力”，但在 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
于 2014-12-01T00:15:19.873 回答