0

我目前在我的家庭作业中陷入循环不变证明。我需要证明其正确性的算法是：

Multiply(a,b)
    x=a
    y=0
    WHILE x>=b DO
        x=x-b
        y=y+1
    IF x=0 THEN
        RETURN(y)
    ELSE
        RETURN(-1)

我试着看几个循环不变量的例子，我对它应该如何工作有了一些了解。然而，在上面的这个算法中，我有两个退出条件，我对如何在循环不变证明中处理这个问题有点迷茫。特别是我正在努力解决的终止部分，围绕 IF 和 ELSE 语句。

到目前为止，我所构建的只是查看算法的终止，在这种情况下，如果x = 0它返回y包含n(while 循环中的迭代次数) 的值的值，其中 if xis not 0，x < b然后它返回-1。我只是有一种感觉，我需要以某种方式证明这一点。

我希望有人可以为我提供一些帮助，因为我在这里找到的类似案例还不够。

非常感谢您抽出宝贵的时间。

4

2 回答 2

2

假设算法终止（让我们假设a>0和b>0，这就足够了），一个不变量是在循环的每次迭代中while，你都有x + by = a.

证明：

  • 起初，x = a所以y = 0没关系
  • If x + by = a, then (x - b) + (y + 1)b = a, 是下一次迭代的x和的值y

插图：

    Multiply(a,b)
        x=a
        y=0
        // x + by = a, is true
        WHILE x>=b DO
            // x + by = a, is true
            x=x-b // X = x - b
            y=y+1 // Y = y + 1
            // x + by = a
            // x - b + by + b = a
            // (x-b) + (y+1)b = a
            // X + bY = a, is still true
        // x + by = a, will remain true when you exit the loop
        // since we exited the loop, x < b
        IF x=0 THEN
            // 0 + by = a, and 0 < b
            // y = a/b
            RETURN(y)
        ELSE
            RETURN(-1)

该算法a/b在b除以时返回a，-1否则返回。Multiply听起来不太像一个合适的名字......

于 2018-10-26T15:24:11.073 回答
0

如果没有确切说明该功能应该做什么，我们无法证明正确性，我在您的问题中找不到。甚至函数的名称也无济于事：如前所述，您的函数在大多数情况下返回 a/b b，a否则-1。Multiply 是一个不恰当的名称。

此外，如果b=0和a>=b“算法”不会终止，所以它甚至不是算法。

正如 Alex M 所指出的，循环的循环不变量是x + by = a. 在循环退出的那一刻，我们还有x < b. 没有其他保证，x因为（大概）a可能是负面的。如果我们保证aandb是正数，那么我们可以保证0<=x<b在循环退出的那一刻，这意味着它实现了带余数除法算法（在循环结束时，y是商和x是余数，并且它终止通过“无限下降”类型参数：正整数的递减序列x必须终止）。然后您可以得出结论，如果x=0,b将 a 整除，则返回商，否则-1返回。

但这不是证明，因为我们缺乏算法应该做什么的规范，以及对其输入的限制的规范。（a 和 b 是任何正整数吗？不允许有负数和 0？）

于 2018-10-26T16:37:42.507 回答