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

我想我理解 0

但我不明白为什么 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 的任何一种情况，循环控制将为 false，因此该情况将导致循环停止。

Answer 2

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

在循环不变量

所在的点，此表达式（循环不变量）保证为 true：

0 < m < n < ASIZE OR m == n OR m == n+1

但是，这（"您理解的部分"）并不总是正确的：

0 < m < n < ASIZE

为什么？因为m递增，n递减，因此m < n可能不再是真的。

这就是为什么您需要"放大"循环不变性，使其始终为真，包括这些情况，m == n和m == n+1，这些情况可能在循环的正常执行过程中出现。

因此，如果你说不变量只是"你理解的部分"，那你就错了——你的循环不变量会失败，这是（根据定义）不行的。

Answer 3

记下 2 个过程案例 - 数组的偶数和奇数长度。例如，创建一个表，其中包含迭代次数、数组以及 itera 之前的 m 和 n 值。我相信自己做并逐行执行代码是最简单的（表格本身在理解整个问题方面可能不如这样做那么有帮助）。

附言。不变性似乎太弱，无法建立后置条件。