Correctness proof by using Loop Invariants 2

Nitroblue 1·2일 전

알고리즘 by Shim 교수님

Computer Science Basics

목록 보기

22/28

Merge Sort

Divide and Conquer

핵심 성질

Divide : 더 작은 동일 문제로 나눈다.

Conquer : 재귀로 해결한다.

Combine : 부분해를 combine하여 전체해로 만든다.

merge sort에서의 Divide and conquer 접목

Divide
-> 정렬할 n개의 원소로 이루어진 수열을 각각 n/2개의 원소를 가지는 2개의 부분수열로 나눈다.

Conquer
-> 두 개의 부분수열을 merge sort을 통해 재귀적으로 정렬한다.

Combine
-> 두 개의 정렬된 부분수열을 merge하여 전체가 정렬된 정답을 만든다.

Merge Procedure

It merges them to form a single sorted subarray that replaces the current subarray A[p...r].

we assume that the subarray A[p...q] and A[q+1...r] are in sorted order.

MERGE(A, p, q, r) 보조 함수로 해당 기능을 수행한다.

MERGE(A, p, q, r)	A : p ~ r
n1 = q - p + 1
n2 = r - q

Let L = [1 ... n1 + 1] and R = [1 ... n2 + 1]
for i = 1 to n1
	L[i] = A[p + i - 1]
for j = 1 to n2
	R[j] = A[q + j]

L[n1 + 1] = Inf
R[n2 + 1] = Inf
i = 1
j = 1
for k = p to r
	if L[i] <= R[j]
		A[k] = L[i]
		i++
	else
		A[k] = R[j]
		j++

Correctness of Merge Procedure

Loop Invariant(L.I)
-> At the start of each iteration for the merging loop, the subarray A[p...k-1] contains the (k - p) smallest elements of L[1...n1+1] and R[1...n2+1], in ascending order.
-> Moreover, L[i] and R[j] is the smallest element of their arrays that have not been copied back into A.

Initialization

첫 루프 진입 전 k는 p이고, i와 j는 모두 1이다. 이를 Loop invariant에 넣어보자.

At the start of each iteration for the merging loop, the subarray A[p...p-1] contains the (p - p = 0) smallest elements of L[1...n1+1] and R[1...n2+1], in ascending order.
-> A[p...p-1]은 공집합이다.
-> 이 집합은 0개의 가장 작은 원소들(in L, R)을 갖고 있다.

Moreover, L[1] and R[1] is the smallest element of their arrays that have not been copied back into A.
-> A는 공집합이므로 아무것도 복사되지 않았으며, 처음에 merge procedure에서 "we assume that the subarray A[p...q] and A[q+1...r] are in sorted order."를 언급했으므로 L[1]과 R[1]은 각 배열에서 복사되지 않은 가장 작은 수임을 보장한다.

따라서 Initialization은 L.I를 만족한다.

Maintenance

복습 : "If it is true before an iteration of the loop, it remains true before the next iteration.

Loop 내에 두 가지 경우가 존재하므로 각각에 대해 증명해야 한다.

When L[i] <= R[j]

루프 시작 전에 L.I가 만족한다고 하자.

At the start of each iteration for the merging loop, the subarray A[p...k-1] contains the (k-p) smallest elements of L[1...n1+1] and R[1...n2+1], in ascending order.

Moreover, L[i] and R[j] is the smallest element of their arrays that have not been copied back into A.
-> L[i]는 A에 복사되지 않은 가장 작은 원소이다.
-> A[p...k-1]이 k-p개의 가장 작은 원소들을 갖고 있기 때문에, L[i]를 A[k]에 넣게 되면 A[p..k]는 k-p+1개의 가장 작은 원소들을 갖고 있게 된다.
-> 이제 다음 iteration 시작 시, k와 i가 증가하면 L.I가 다시 만족한다.

When L[i] > R[j]

위의 경우와 같다.

따라서 Maintenance는 L.I를 만족한다.

Termination

루프 탈출 후 k = r + 1이다.

이를 L.I에 대입해보자.

the array A[p...r] contains the (r-p+1) smallest elements of L[1...n1+1] and R[1...n2+1], in sorted order.
-> L과 R의 총 사이즈는 n1 + n2 + 2 = r - p + 3 이다.
-> 아직 복사되지 않은 두 개의 원소들은 각 배열의 가장 큰 원소이자 sentinel인 원소들이다.

Moreover, L[n1+1] and L[n2+1] is the smallest element of their arrays that have not been copied back into A.
-> L[n1+1]과 R[n2+1]은 각각 Inf이며, 복사되지 않은 유일한 원소이다.