c - 循环不变证明理解

Question

我正在尝试学习 C 中的循环不变量。我有一个代码并且我有循环不变量，但我不完全理解为什么。这是代码:

/* 0 ≤ m < n < ASIZE AND A[m] ≥ A[m+1] ≥ ... ≥ A[n] */
void ReverseArray(int A[], int m, int n)
{
  int temp;
  while (m < n)
  {
        temp = A[m]; A[m] = A[n]; A[n] = temp;
        m++;
        n--;
        /* loop invariant: 0 < m < n < ASIZE OR m == n OR m == n+1 */
} 
}
/* for the initial values of m and n, A[m] ≤ A[m+1] ≤ ... ≤ A[n] */

循环不变量是: 0 < m < n < ASIZE OR m == n OR m == n+1

我想我理解 0 < m < n < ASIZE。这将是因为 while 循环，它说 m 不能为 0 但它必须小于 n。并且 n 必须小于数组大小。

但我不明白为什么 m == n 和 m == n+1。

有什么想法吗？

Answer 1

如果在循环体之前，则是 m + 1 == n ，然后在循环结束时，m将增加和 n将被递减。此时，m == n + 1 .

例如，当 m值为 2，并且 n值为 3。然后在 m++; n--; 之后, m具有值 3 和 n值为 2。

如果在循环体之前，则是 m + 2 == n ，然后在循环体之后，m == n .例如，如果 m具有值 2 和 n值为 4，然后是 m是 3 和 n是 3。

对于在循环体之后结果为 m == n 的任何一种情况或 m == n + 1 ，循环控制将为假，因此这种情况将导致循环停止。