Корректность программы для программы кубической сортировки - PullRequest
Новая
       30

Корректность программы для программы кубической сортировки

0 голосов
/ 04 ноября 2019

Мне нужна помощь в доказательстве инварианта моего цикла для моей программы кубической сортировки python.

До сих пор я вычислял инвариант цикла, который состоит из двух частей

  1. 0 <= i + 1 <= len (L) </li>
  2. L [0: i+1] отсортировано. 
def cubicSort(L):
    i = 0
    while i + 1 < len(L):
        if L[i] > L[i + 1]:
            L[i], L[i + 1] = L[i + 1], L[i] # That is, swap L[i] and L[i + 1].
            i = 0
        else:
            i = i + 1

предварительное условие: L - список целых чисел в сообщении: список переставлен и отсортирован

Не знаю, какподойти к доказательству

1 Ответ

1 голос
/ 10 ноября 2019

Есть два элемента доказательства правильности: вы должны доказать, что когда алгоритм завершается, результат верен;и вы должны доказать, что алгоритм завершает работу.

Оба ваших инварианта цикла верны, но вам нужно доказать, что они являются инвариантами. Чтобы показать это, вы должны показать, что они верны до первой итерации цикла, и если они верны до некоторой итерации, то они будут истинны после этой итерации.

После того, как это будет сделано, просто, когдацикл завершается, i + 1 == len(L) и, следовательно, L[0:i+1] равен L, поэтому из этого следует, что L сортируется после завершения цикла.

Обычно проще показать, что алгоритмзавершается путем нахождения варианта цикла - целочисленного значения, которое уменьшается на каждой итерации цикла и которое приводит к завершению цикла, когда количество достигает 0. Но для этого алгоритма не существует очевидного вариантапоскольку счетчик цикла i в цикле сбрасывается на 0, это означает, что эта переменная не просто монотонно увеличивается или уменьшается.

Ключом к этому доказательству является учет числа инверсии в списке, где «инверсия» означает пару элементов списка, которые находятся вне заказ. На каждой итерации либо i увеличивается, либо i сбрасывается в 0, но число инверсий уменьшается на 1. Невозможно, чтобы i продолжал увеличиваться, а количество инверсий становилось меньшебез i достижения границы цикла while или числа инверсий, достигающих 0. Если в списке не осталось инверсий, L[i] > L[i + 1] всегда ложно, поэтому i будет продолжать увеличиваться до границыи затем цикл завершается, как требуется.

...