如何证明Hoare快速适用于任何阵列

Question

试图找出为什么Hoare快速排序正常工作。基本上我无法向自己证明我们无法创建一个会导致Hoare排序算法失败的数组。证明没有必要成为100％数学。我只想相信算法有效。

在下面的代码中，我重写了算法的一些部分，以使我更清楚（基本的想法保持不变）。

void quickSort(int[] arr, int start, int end) {
  int pivotIndex = partition(arr, start, end);

  if (start < pivotIndex - 1) quickSort(arr, start, pivotIndex - 1);
  if (end >= pivotIndex) quickSort(arr, pivotIndex, end);
}

int partition(int[] arr, int leftIndex, int rightIndex) {
    int pivot = arr[(leftIndex + rightIndex) / 2];

    while (true) {
        while (arr[leftIndex] < pivot) leftIndex++;
        while (arr[rightIndex] > pivot) rightIndex--;

        if (leftIndex == rightIndex) return leftIndex + 1;

        if (leftIndex < rightIndex) {
          swap(arr, leftIndex, rightIndex);
          leftIndex++;
          rightIndex--;
        }
        if (leftIndex > rightIndex) return leftIndex;
    }
}

我对这个功能100％肯定：

1. 函数应该将数组分成两个子数组 low - 包含小于或等于pivot的元素 high - 包含更大或更合适的元素
2. 分区完成后，leftIndex不能大于rightIndex大于1.换句话说：leftIndex - rightIndex只等于0或1。
3. 函数始终返回高子数组中第一个元素的第一个索引

我完全不明白的是：

First question:

为什么如果代码

if (leftIndex < rightIndex) { 
    swap(arr, leftIndex, rightIndex);
    leftIndex++;
    rightIndex--;
}

已执行，之后leftIndex变为等于rightIndex，这并不意味着数组已成功分区，我们可以返回leftIndex + 1？为了澄清我的想法，请看下面的代码：

int partition(int[] arr, int leftIndex, int rightIndex) {
    int pivot = arr[(leftIndex + rightIndex) / 2];

    while (true) {
        while (arr[leftIndex] < pivot) leftIndex++;
        while (arr[rightIndex] > pivot) rightIndex--;

        // remove line from here    
        //if (leftIndex == rightIndex) return leftIndex + 1;

        if (leftIndex < rightIndex) {
          swap(arr, leftIndex, rightIndex);
          leftIndex++;
          rightIndex--;
        }
        // move it here. If I do that, code stop working and sort array in a wrong way
        //sorce array: [6, 3, 12, 10, 3, 8, 5, 8, 11, 2, 9]
        //final array: [2, 3, 3, 5, 6, 8, 8, 9, 10, 12, 11] - 12 and 11 at wrong places
        if (leftIndex == rightIndex) return leftIndex + 1;

        if (leftIndex > rightIndex) return leftIndex;
    }
}

Second question:

让我们对以下场景进行成像。假设枢轴值为10，并且下面的代码已成功执行：

    01 while (arr[leftIndex] < pivot) leftIndex++;
    02 while (arr[rightIndex] > pivot) rightIndex--;
    03 if (leftIndex == rightIndex) return leftIndex + 1;

之后，假设leftIndex和rightIndex停留在索引为X且值为6的元素，即arr [X] - > 6.第3行将返回索引X + 1的值，让我们说8.所以基本上我们将有子数组：

[..., ...] and [8, ..., 10, ...]

所以高子数组将包含小于pivot的元素。是否可以创建此类阵列来复制该场景？

Answer 1

这可能会回答您关于如何证明Hoare算法的整体问题。 This online PDF gives正式和非正式证明。这是非正式的（它是一个图像因为pdf没有文本，它只是一个图像本身）：