2

我正在尝试了解 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。

有什么想法吗？

4

3 回答 3

1

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

在定位循环不变量时，这个表达式（循环不变量）保证为真：

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

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

0 < m < n < ASIZE

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

这就是为什么您需要“放大”循环不变量以使其始终为真，包括这些情况m == n和m == n+1，这可能在循环的正常执行期间出现。

因此，如果您说不变量只是“您理解的部分”，那您就错了-您的循环不变量将失败，这（根据定义）是禁忌。

于 2013-10-03T16:58:32.703 回答
1

写下 2 个过程案例 - 数组的偶数和奇数长度。例如，创建一个包含迭代次数、数组以及迭代次数和迭代次数之前的值的m表n。我相信最简单的做法是自己完成并逐行编写代码（表格本身可能对理解整个问题没有太大帮助）。

PS。不变量似乎太弱而无法建立后置条件。

于 2013-10-03T16:58:59.383 回答
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 == norm == n + 1的任何一种情况，循环控制将为假，因此这种情况将导致循环停止。

于 2013-10-03T16:59:51.110 回答