algorithm - QuickSort パーティションのループ不変式

Question

Quicksort アルゴリズムの一部の実装について、ループ不変条件の定義と証明に問題があります。これはロムート版でもホアレ版でもありません。

このように実装されている既知のバージョンの 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、 array 内の各インデックスに対してA:

• もしk = pそうならA[k] = y

• もしp < k <= iそうならA[k] < y

• もしj <= k <= rそうならA[k] > y

whileループインpartition()メソッドのループ不変条件を定義して（上記が間違っている場合）、それを証明するのを手伝ってください。