3

ループ不変条件とは何ですか? また、それらを使用してヒープ ソート アルゴリズムの正しさを証明するにはどうすればよいですか?

4

3 に答える 3

8

ループ不変条件は、アルゴリズムまたは一連の命令が正しいかどうかを証明するための非常に単純ですが強力な手法です。それらは繰り返しで素晴らしく機能します。

不変プロパティを設定します。これは、実行中に維持したい反復で望ましいプロパティです。たとえば、正しい状態で開始し、アルゴリズムの過程でそれを維持した場合、正しいアルゴリズムがあることがわかります

したがって、目的のプロパティ、つまり不変性があることを 3 つのステップで示す必要があります。

私。初期化: ループの反復の最初のステップで、アルゴリズムの不変特性があることを示すことができますか?

ii. 保守: 不変性を維持していますか? その時点までの反復で真だった場合、次の反復でも真ですか?

iii. 終了: ループが最終的に終了すると、不変条件を使用して、作成したアルゴリズムが正しいことを示します。

BuildMaxHeap は HeapSort アルゴリズムで使用されるため、この知識を使用して BuildMaxHeap が正しいことを証明しましょう。

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 まで低下し、ループ不変式によって、各ノードが最大ヒープのルートになると終了します。

したがって、あなたが書いたアルゴリズムは正しいです。

Introduction to Algorithms (CLRS) には、この手法の非常に優れた取り扱いがあります。

于 2010-12-06T09:44:42.367 に答える
1

ループ不変条件は、ループの実行中に変化しない「法則」です。
ヒープ ソート - 不変条件は、すべてのノードにヒープ プロパティがあることです。つまり、ノードの値は、その左右の子の値よりも大きくなります。

于 2010-12-06T09:29:39.977 に答える