这段代码的循环不变量是什么？答案

【问题标题】：What is the loop invariant for this code?这段代码的循环不变量是什么？
【发布时间】：2015-08-10 09:45:19
【问题描述】：

数组包含先增加值然后减少值的整数。目前尚不清楚数字何时开始减少。编写高效的代码，将第一个数组中的数字复制到另一个数组中，以便第二个数组按升序排序。

代码如下：

int _tmain(int argc, _TCHAR* argv[])
{
    int a[10] = { 17, 24, 31, 39, 44, 49, 36, 29, 20, 18 };
    int b[10];

    int i = 0, j = 9, k = 0;

    while (i <= j) {
        if (a[i] < a[j]) {
            b[k++] = a[i++];
        }
        else {
            b[k++] = a[j--];
        }
    }

    return 0;
}

这里的循环不变量是什么？

【问题讨论】：

标签： c nomenclature loop-invariant

【解决方案1】：

循环不变量是在循环的每次迭代之前和之后都成立的东西。这包括循环终止之后和开始之前。它们中有不少，尽管它们中的大多数并不重要。您将需要选择一个有助于证明算法正确的算法。一个循环不变量是：

长度为 k 的子数组 b 由数组 a 中的项目组成，但按排序顺序。

在证明这个不变量时，您需要为数组 b 显示元素 i+1 大于元素 i。

【讨论】：

为了更好地反映这个不变量，也许我应该有 k = -1 作为初始化和 b[++k] 在赋值
@Abhiram k 转到 10 确实会造成问题（尽管想法相同）。如果您愿意，我可以将其更改为“长度为 k 的子数组”，这将起作用并反映您的代码，但会更加抽象。

【解决方案2】：

不变量是while循环中的条件，所以i <= j。

循环的不变量是在之前（和之后）保持的属性每次重复

来源：wiki

【讨论】：

循环终止时不成立。
如果你把它改正为i <= j + 1，那么它是一个不变量，而不是the不变量，因为它不足以证明循环结束后，输出数组按升序排列。