循环不变量（java）答案

【问题标题】：Loop invariant (java)循环不变量（java）
【发布时间】：2015-01-27 03:45:22
【问题描述】：

我有以下代码来反转整数中的数字：

public class integerReversal {
    public static int reverseNum(int number){
        int reversed = 0;
        int remainder;
        //{I:  ; B: number > 0}
        while (number > 0){
            remainder = number % 10;
            number = number / 10;
            reversed = reversed * 10 + remainder; 
        }
        //{I: ; !B: number == 0}
    return reversed;
    }
    public static void main (String [] args){ 
        System.out.println(reverseNum(1262015 ));
    }
}

我的教授要求我们编写这段代码，还说要编写循环不变量和循环条件。我了解这里的循环条件，我只是不确定我应该看什么不变量。我意识到在 while 循环的开始和结束时某些条件是正确的，对于每次迭代，我只是看不出它会是什么。提示将不胜感激。

【问题讨论】：

您的教授似乎希望您使用不同的循环，例如 for，循环上方的注释暗示了 for 循环。
评论是我自己的；我的教授指定我们应该使用一个while循环来写这个。那注释表明它应该是一个for循环呢？

标签： java loops loop-invariant

【解决方案1】：

在您的情况下，reverse >=0 是您的循环不变式，因为无论您是否中断循环，它都将始终保持正确。

【讨论】：

这是我最初的猜测，但似乎有点微不足道。经常这样吗？
循环不变量是对循环的每次迭代都成立的条件。在您的循环中，谓词 reversed >= 0 是循环不变量，因为它始终为真。
如果它回答了您的问题，请接受答案，如果您有任何疑问，请告诉我。谢谢。
@AnindaBhattacharyya 恐怕你不太了解循环不变量
@sprinter 感谢您对我的知识发表评论，但我相信我们不要在这方面浪费时间和精力，因为我非常了解我的知识，并尝试专注于我们的答案。

【解决方案2】：

循环不变量是一个常量表达式，其中包含旨在更改每次迭代的值。

在您的每次迭代中，number 是没有最右边数字的数字，reversed 是您从先前迭代中的余数构建的数字。所以我相信答案是，在每次迭代中，以下表达式保持不变：

number * 10 + reverseNum(reversed)

换句话说，您可以随时通过反转您当前的解决方案并添加 10 * 当前数字来取回原始数字。

这种不变量在测试您的算法时非常有用 - 一些编码人员会定期包含 assert 语句来测试这些类型的不变量。

可能有几个不变量 - 在您的情况下，有许多不等式仍然成立。

【讨论】：