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

Question

数组包含值先递增后递减的整数。目前还不知道从什么时候开始数量减少。编写高效代码，将第一个数组中的数字复制到另一个数组中，使第二个数组按升序排序。

代码如下:

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

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

Answer 1

循环不变量在每次循环迭代之前和之后都为真。这包括循环结束之后和开始之前。有相当多的人，尽管他们中的大多数都不重要。你会想要选择一个有助于证明算法是正确的。循环不变量应该是:

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

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

Answer 2

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

循环的不变量是一个保存before(和after)的属性。每个重复

来源:维基