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

Question

我目前在家庭作业中遇到循环不变性证明问题。我需要证明其正确性的算法是:

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 循环中的迭代次数)，其中好像 x不是 0 , 和 x < b然后返回 -1 .我只是觉得我需要以某种方式证明这一点。

我希望有人能帮我分享一些关于这方面的信息，因为我在这里发现的类似案例还不够。

非常感谢您的宝贵时间。

Answer 1

如果算法终止(为此，我们假设 a>0 和 b>0，这就足够了)，一个不变的是在您的每次迭代中 while 循环，你有 x + by = a。

证明:

• 一开始，x = a 和 y = 0 所以没关系
• 如果x + by = a，则(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)

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