Loop Invariant用于计算阶乘的函数

Question

我很难正确识别以下函数的循环不变量:

F(y)
    X <-- 1
    while (y > 1)
        do x <-- x * y
           y <-- y - 1
    return (x)

我已经确定了循环不变量,x = 1 OR x = y!因为该语句作为前置条件保持为真,并且作为后置条件保持为真.

它似乎并不适用于每次迭代,例如,如果y = 3,那么在循环的第一次迭代中,x = 1*3,相当于3和NOT 3!相当于6.

这就是我猜想我的困惑.一些书籍文章声明循环不变量是一个必须在开头或循环(因此是前置条件)等于true的语句,并且必须在循环结束时保持为真(因此在条件后)但不一定需要在循环中保持正常.

上述函数的正确循环不变量是多少？

Answer 1

可能的循环不变量是x⋅y!= y ₀!其中y ₀是传递给函数的y的初始值.无论循环的迭代次数已经完成多少次,此语句始终为true.

在循环开始之前必须保持一个前提条件,在循环结束后必须保持后置条件,并且无论循环完成多少次迭代,都必须保持不变量(这就是为什么它被称为"不变" - 它没有'改变它是真的).

通常,同一循环可能存在不同的可能不变量.例如,对于任何循环,1 = 1将是一个真值,但为了显示算法的正确性,您通常必须找到更强的不变量.