Использование инвариантов цикла для доказательства правильности сортировки кучи - PullRequest
Новая
       18

Использование инвариантов цикла для доказательства правильности сортировки кучи

3 голосов
/ 06 декабря 2010

Что такое инварианты цикла и как их использовать для доказательства правильности алгоритма сортировки кучи?

Ответы [ 3 ]

8 голосов
/ 06 декабря 2010

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

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

Таким образом, вам нужно будет показать, что у вас есть желаемое свойство, неизменность за 3 шага:

я. Инициализация : Можете ли вы показать, что у вас есть свойство инварианта алгоритма на первом шаге итерации цикла?

II. Техническое обслуживание : Поддерживаете ли вы неизменность? Если это было верно для итерации до этого момента, верно ли это для следующей итерации?

iii. Завершение : Когда ваш цикл окончательно завершится, будет использован инвариант, чтобы показать, что написанный вами алгоритм верен.

Давайте использовать это знание, чтобы доказать, что BuildMaxHeap верен, поскольку он используется в алгоритме HeapSort. 

BuildMaxHeap(A)
  heap-size[A] = length[A]
   for i : length[A]/2 to 1
       Max-Heapify(A, i)

Источник. CLRS

Например, как мы узнаем, что построение максимальной кучи фактически создает максимальную кучу! Если наш алгоритм BuildMaxHeap работал правильно, мы могли бы использовать его для правильной сортировки.

Следуя нашей вышеупомянутой интуиции, нам нужно выбрать желаемое свойство, которое мы сохраняем на протяжении всего алгоритма. Какое свойство желательно в MaxHeap? куча [i]> = куча [i * 2]. Независимо от того, сколько вы возитесь с кучей, если у нее все еще есть это свойство, то это MaxHeap.

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

Инициализация: до первой итерации. Все это лист, значит, это уже куча.

Обслуживание: допустим, у нас есть рабочее решение до сих пор. Дочерние узлы i пронумерованы выше, чем i. MaxHeapify также сохраняет инвариант цикла. Мы поддерживаем неизменность на каждом этапе.

Завершение: Завершается, когда значение i уменьшается до 0, и по инварианту цикла каждый узел является корнем max-heap.

Следовательно, алгоритм, который вы написали, верен.

Введение в алгоритмы (CLRS) очень хорошо трактует эту технику.

1 голос
/ 06 декабря 2010

Инвариант цикла - это «закон», который не изменяется во время выполнения цикла.
В сортировке кучи - инвариант состоит в том, что у каждого узла есть свойство кучи, то есть значение в узле больше, чем значения его левого и правого потомков.

0 голосов
/ 20 января 2017

Корректность BuildMaxHeap

• Инвариант цикла: В начале каждой итерации цикла for каждый узел i + 1, i + 2, ..., n является корнем max-heap.

• Инициализация: - до первой итерации i = ⎣n / 2⎦ –Ноды ⎣n / 2⎦ + 1, ⎣n / 2⎦ + 2, ..., n - листья, следовательно, корни тривиальных max-куч.

• Обслуживание: - По LI, поддеревья у дочерних узлов узла i являются максимальными кучами. –Hence, MaxHeapify (i) отдает узлу i корень максимальной кучи (при сохранении свойства корня максимальной кучи узлов с большими номерами). –Уменьшение i восстанавливает инвариант цикла для следующей итерации.

...