java - 以第一个元素为基准，为什么索引 i 不会超出数组的边界？

Question

在partition方法的两个while循环里面，为什么乍一看好像没有考虑索引i是否超出数组的边界？[这是Big Java的正确代码，我已经测试过了，只是索引的东西让我感到困惑]

public void sort(int from, int to)
   {
      if (from >= to) return;
      int p = partition(from, to);
      sort(from, p);
      sort(p + 1, to);
   }

   private int partition(int from, int to)
   {
      int pivot = a[from];
      int i = from - 1;
      int j = to + 1;
      while (i < j)
      {
         i++; while (a[i] < pivot) i++;//here
         j--; while (a[j] > pivot) j--;//here
         if (i < j) swap(i, j); 
      }
      return j;
   }

Answer 1

由于枢轴是从同一个数组中选择的，并且由于算法逻辑的实现方式，您永远不需要检查索引是否超出范围。在执行的某个时刻，条件必须变为真。

算法的正确性可以用循环不变量来证明。

1. private int partition(int from, int to)
2. {
3.    int pivot = a[from];
4.    int i = from - 1;
5.    int j = to + 1;
6.    while (i < j)
7.    {
8.        i++; 
9.        // at least one of a[i]...a[to] is greater than or equal to pivot 
10.       while (a[i] < pivot) i++;
11.       j--; 
12.       // at least one of a[from]...a[j] is less than or equal to pivot
13.       while (a[j] > pivot) j--;//here
14.       if (i < j) swap(i, j);
15.       // if i < j then at least one of a[i + 1]...a[to] is greater than or equal to pivot
16.       // if i < j then at least one of a[from]...a[j - 1] is less than or equal to pivot
17.   }
18.   return j;
19. }

第 9 行和第 12 行(以及第 15、16 行)包含适用于循环 6 到 17 的每次迭代的不变量。从这些不变量可以清楚地看出 i和 j索引永远不能超出数组边界。

我们只能证明第9行的不变量，第12行的不变量可以类推证明。

对于第 1 次迭代，它为真，因为枢轴被选为 a[from]和 i = from .

在每次迭代(包括第一次迭代)结束时，我们将元素移动到位置 i大于或等于 pivot 到位置 j .因为i < j那么第 15 行的不变量成立。在递增 i 后的下一次迭代中在第 8 行，不变量 9 变为有效，它直接来自不变量 15。通过归纳我们可以得出结论，不变量 9 在循环 6 到 17 的每次迭代中都是有效的。

如果我们选择 pivot 作为数组的最后一个元素，即 a[to]，不变量仍然成立。但是，我们需要更改排序方法中的流程。

sort(from, p == to ? p - 1 : p);
sort(p + 1, to);

代替

sort(from, p);
sort(p + 1, to);