时间戳

首页 > 解决方案 > 乘法算法的循环不变证明

algorithm - 乘法算法的循环不变证明

问题描述

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

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。我只是有一种感觉，我需要以某种方式证明这一点。

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

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

标签： algorithmpseudocodediscrete-mathematicsloop-invariant

解决方案

假设算法终止（让我们假设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听起来不太像一个合适的名字......

推荐阅读