algorithm - QuickSort分区的循环不变量

Question

我在为某些快速排序算法的实现定义和证明循环不变量 时遇到问题。这既不是 Lomuto 的也不是 Hoare 的分区版本。

如果您知道以这种方式实现的某些已知版本的快速排序，请告诉我。

算法在 Python 中的实现:

def partition(arr: list, p: int, r: int):
    y = arr[p]
    i = p
    j = r + 1

    while i < j:
        i = i + 1

        while i <= r and A[i] < y:
            i = i + 1

        j = j - 1

        while j >= p and A[j] > y:
            j = j - 1

        if i <= j:
            swap(arr, i, j)

    swap(arr, j, p)

    return j


def quicksort(arr: list, p: int, r: int):
    if p < r:
        q = partition(arr, p, r)
        quicksort(arr, p, q - 1)
        quicksort(arr, q + 1, r)


def swap(arr: list, i, j):
    tmp = arr[i]
    arr[i] = arr[j]
    arr[j] = tmp

我已经设法定义了以下循环不变量(它可能不正确):

At the beginning of each iteration of the while loop, for each index k in array A:

• if k = p, so A[k] = y

• if p < k <= i, so A[k] < y

• if j <= k <= r, so A[k] > y

请帮我为 while 定义一个循环不变式循环 partition()方法(如果上述不正确)，并证明。

Answer 1

外层 while 的不变量表示到目前为止已扫描的数组部分，即范围 A[p..i] 和 A[j..r]，左边元素不大于pivot，右边元素不小于pivot。 (当然，A 的内容是初始内容的排列。)

当循环退出时，所有左侧元素都不大于所有右侧元素，因此 A[p..r] 被分区。