Нужна помощь в проверке инварианта цикла (простая сортировка пузырьков, частичная корректность)

Question

Алгоритм сортировки пузырьков (псевдокод):

Input: Array A[1...n]
for i <- n,...,2 do
    for j <- 2,...,i do
        if A[j - 1] >= A[j] then
            swap the values of A[j-1] and A[j];

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

Инвариант цикла: после каждой итерации i самые большие элементы i - n + 1 в A находятся в том положении, в котором они были бы отсортированы без убывания. В случае если массив A содержит более одного максимального значения, пусть самый большой элемент будет элементом с наименьшим индексом из всех возможных максимальных значений.

Индукционный базис (i = n): внутренний цикл выполняет итерацию по каждому элементу A. В конце концов, j указывает на наибольший элемент. Это значение будет меняться, пока не достигнет позиции i = n, которая является самой высокой позицией в массиве A и, следовательно, конечной позицией для наибольшего элемента A.

Шаг индукции: (i = m -> i = m - 1 для всех m > 3): внутренний цикл выполняет итерации по каждому элементу A. В конце концов, j указывает на наибольший элемент из тех, которые еще не отсортированы. Это значение будет меняться, пока не достигнет позиции i = m - 1, которая является самой высокой позицией позиций, еще не отсортированных в массиве A, и, следовательно, конечной позицией для наибольшего еще не отсортированного элемента A.

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

Answer 1

Я был бы склонен пересмотреть ваше доказательство в следующих терминах: Bubble sort A[1..n]: for i in n..2 for j in 2..i swap A[j - 1], A[j] if they are not already in order

Инвариант цикла: пусть P(i) <=> для всех k st i

Базовый случай: изначально i = n и инвариант P (n) тривиально выполняется.

Шаг индукции: предполагая, что инвариант выполняется для некоторого P(m + 1), покажите, что после выполнения внутреннего цикла инвариант выполняется для P (m).