这段代码的循环不变量是什么?

What is the loop invariant for this code?

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

代码如下:

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;
}

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

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

an invariant of a loop is a property that holds before (and after) each repetition

来源:wiki

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

The sub-array b of length k consists of the items from array a, but in sorted order.

在证明这个不变量时,您需要为数组 b 证明元素 i+1 大于元素 i.