使用循环不变量证明简单算法的正确性

Question

我正在尝试学习循环不变技术以生成更高效的算法。我对通过评估循环不变量来证明正确性的理解是循环不变量必须在迭代前和迭代后为真，以确认想要的输出。

对于我在下面组合的算法（按降序对序列进行排序）- 这是属性我认为满足正确性确认：

“目标是递减序列，使得从 0 到 j-1 的所有 i 的 A[j] > A[i]”

我也认为 i >=0 和 i < A.length 在这种情况下将是循环不变量。

在检查循环不变量的三个步骤（初始化、维护、终止）时……我想出的东西在这种情况下有意义吗？我觉得我仍然不太了解如何在这种情况下应用这个概念。

static void Sort(int array[]) {
  int size = array.length; 
  
  for (int i = 0; i < size - 1; i++)
   
     for (int j = i + 1; j < size; j++)
     
        if (array[j] > array[i]) {
        
           // swapping elements. 
           int buffer = array[j];
           array[j] = array[i];
           array[i] = buffer;
           
        }

Answer 1

有一个“背景不变量”说数组的内容只是置换（没有修改、抑制或添加值）。唯一修改数组的操作是交换这一事实保证了不变性。

现在，观察内循环仅处理从 i 开始的元素，其中 i 递增。这意味着数组的初始部分（直到 i-1） 必须是 已排序序列的开始。这是外循环的不变量。所以内层循环的目的是找到排序后的序列的下一个元素，并将其带到i.

的位置

这将我们引向内循环的不变量，它表示插槽 i 包含目前所见值中的最小值，即在 i..j.[=21 范围内=]

插图：

如果我们将算法应用于数组

6 8 1 3 4 7 0 9

我们可以肯定的是，在执行了两次外层循环之后，数组将以

开头

1 3

由于数组的其余部分可能已被打乱，因此很难预测内循环中接下来会发生什么。

无论如何，在外循环的第一次迭代期间，在内循环的三次迭代之后，我们知道第一个值将是

因为它是最小的

6 8 1

  for (int i = 0; i < size - 1; )
     // array[0..i-1] is the prefix of the sorted sequence
     for (int j = i + 1; j < size; )
        // array[i] is the smallest among array[i..j-1]
        if (array[j] > array[i]) {
           // swapping elements. 
           int buffer = array[j];
           array[j] = array[i];
           array[i] = buffer;              
        } 
        // array[i] is the smallest among array[i..j]
        j++;
        // array[i] is the smallest among array[i..j-1]
     }
     // array[0..i] is the prefix of the sorted sequence
     i++;
     // array[0..i-1] is the prefix of the sorted sequence

使用循环不变量证明简单算法的正确性

Using loop invariants to prove correctness of a simple algorithm

algorithm

loops

proof

loop-invariant