루프 불변 상태에 대한 추론과 병합 정렬의 정확성을 증명하려면 어떻게해야합니까? 시각화 할 수있는 유일한 방법은 병합 단계 subarrays (invariants)를 결합하여 상태를 유지할 때 즉, 각 병합 단계에서 다시 정렬됩니다. 그러나 올바르게 진행되는지 여부는 알 수 없습니다. Loop 불변량 및 내용에 대해서는 많이 알지 못합니다. 어떤 사람이 나를이 사실에 대해 깨우칠 수 있습니까? 초기화 b)는 유지 C) 종단루프 불변성을 사용하여 병합 정렬의 정확성을 증명합니다. (초기화, 유지 관리, 종료)
이 많은 의무가) 각 단계
에 무슨 일이 일어날 지 설명하라! 종류
MERGE-SORT 병합에 대한
는의사 (A, P, R)
1 if p < r
2 then q <-- [(p + r)/2]
3 MERGE-SORT(A, p, q)
4 MERGE-SORT(A, q + 1, r)
5 MERGE-SORT(A, p, q, r)
MERGE-SORT (A, P, Q, R) 우리는 시도
1 n1 <-- q - p + 1
2 n2 <-- r - q
3 create arrays L[1 ... n1 + 1] and R[1 ... n2 + 1]
4 for i <-- 1 to n1
5 do L[i] <-- A[p + i - 1]
6 for j <-- 1 to n2
7 do R[j] <-- A[q + j]
8 L[n1 + 1] <-- infinite
9 R[n2 + 1] <-- infinite
10 i <-- 1
11 j <-- 1
12 for k <-- p to r
13 do if L[i] <= R[j]
14 then A[k] <-- L[i]
15 i <-- i + 1
16 else A[k] <-- R[j]
17 j <-- j + 1
두 더미의 카드 더미를 정렬 할 수 있지만 각 기본 단계에서 파일 더미가 비어 있는지 여부를 확인하지 않고 코드를 단순화하기 위해 무한을 센티넬 카드로 사용합니다. 따라서, 센티널 카드 인피니가 노출 될 때마다, 두 더미에 센티넬 카드가 노출되지 않으면 작은 카드가 될 수 없습니다. 그러나 그런 일이 발생하면 모든 비 감시 카드는 이미 출력 파일에 놓여 있습니다. 우리는 정확히 r - p + 1 개의 카드가 출력 더미에 놓여 있음을 알고 있기 때문에, 우리가 많은 기본 단계를 수행하면 멈출 수 있습니다.
루프 불변 :
초기화 : 그 부분 배열 A[p ... k - 1]이 비어 있도록 루프의 첫 번째 반복하기 전에, 우리는 k = p 있습니다. 이 빈 부분 배열은 L과 R의 k - p = 0 작은 요소를 포함하고 i = j = 1 보낸 두 L [I]와 R [J] A.
유지로 다시 복사되지 않은 그들의 배열의 최소 요소가 : 각 반복이 루프 불변성을 유지하는지 확인하기 위해 먼저 l [i] < = R [j]이라고 가정합니다. 그러면 L [i]는 아직 A로 다시 복사되지 않은 가장 작은 요소입니다. 에 k - p의 가장 작은 요소가 포함되어 있기 때문에 14 번째 줄이 A [k]로 L [i]를 복사 한 후에 A[p ... k] 부분 배열에 k - p + 1의 가장 작은 요소가 포함됩니다. k (for 루프 업데이트에서)와 i (15 행에서)를 증가 시키면 다음 반복에 대한 루프 불변 값을 다시 설정합니다. L [i]> R [j] 대신에 16-17 행은 루프 불변성을 유지하기위한 적절한 조치를 수행합니다.
종료 : 종료시 k = r + 1. 루프 불변량에 의해 서브 배열 A[p ... k - 1]은 A[p ... r]이고 L[1 ... n1 + 1]과 R[1 ... n2 + 1]의 가장 작은 요소가 정렬 순서대로 포함되어 있습니다. 배열 L과 R은 함께 n1 + n2 + 2 = r - p + 3 요소를 포함합니다. 두 개의 가장 큰 요소를 제외한 모든 요소가 A로 다시 복사되었으며이 두 가지 가장 큰 요소는 감시 요소입니다.