Инвариант петли раздела QuickSort

Question

У меня проблемы с определением и проверкой инварианта цикла для некоторой реализации алгоритма быстрой сортировки. Это не версия раздела Lomuto и Hoare.

Если вам известна какая-то известная версия Quicksort, реализованная таким образом, сообщите мне, пожалуйста.

Реализация алгоритма в 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

Мне удалось определить следующий инвариант цикла ( это может быть неверно ):

В начале каждой итерации цикла while для каждого индекса k в массиве A:

• , если k = p, поэтому A[k] = y

• , если p < k <= i, поэтому A[k] < y

• , если j <= k <= r, поэтому A[k] > y

Пожалуйста, помогите мне определить инвариант цикла для цикла while в методе partition() (если приведенное выше неверно) и доказать это.

Answer 1

Инвариант внешнего , в то время как выражает, что среди отсканированных на данный момент участков массива, а именно диапазонов A[p..i] и A[j..r], левые элементы не больше, чем сводная точкаи правильные элементы не меньше.(И, конечно, содержимое A является перестановкой исходного содержимого.)

Когда цикл завершается, все левые элементы не больше всех правых элементов, так что A[p..r] разбит на части.