proof of correctness of sorting (정렬에 대한 증명, 정렬이란 무엇인가)
- 입력 : 정수 집합 {a[0], a[1], ... a[n-1]}
- sorting이 끝난 후 배열에 저장된 값들을 {b[0], b[1], ... b[n-1]}이라고 하자 (같은 배열이지만 구별하기 위함
- 조건 1 : {a[0], a[1], ... a[n-1]} = {b[0], b[1], ... b[n-1]} 집합으로 같음
- 조건 2 : b[0] < b[1] ... < b[n-1] - 같은 것이 없다는 가정 하에
Selection sort (선택 정렬)
int sort(int a[], int n){
int i, j, m, t;
for(i = 0; i <n ; i++){
//Find Minimum
m = i;
for(j = i; j < n; j++) if(a[m]>a[j]) m = j;
t = a[i]; a[i]=a[m]; a[m]=t;
}
return;
}
proof of invariant
invariant : k번째 루프가 끝난 후에
- a[0] < a[1] < ... < a[k-1]을 만족한다
- a[k-1] < a[x] if x > k-1을 만족한다
(1) Base : 0번째 루프가 끝난 후에 invariant 모두 null condition → true이다 ∴ invariant 성립
(2) Step :
k번째 루프가 끝난 후에 invariant가 성립한다면 (→P(n-1)) k+1번째 루프가 끝났을 때도 invariant가 성립한다(→P(n))
k번째 루프 : a[k], a[k+1], ... a[n-1] 중 가장 작은 수를 a[k]로 옮기는 역할을 함
k번째 루프가 끝난 후에 invariant가 성립한다고 가정 (믿음)
- a[0] < a[1] < ... < a[k-1]까지 이미 정렬되어있음
- x > k-1이면 a[k-1] < a[x]이다.
k+1번째 루프 :
- a[k-1] < a[x]가 성립하고, k는 어떠한 x 이므로 a[0] < a[1] < ... a[k] < a[k]이 성립함
- a[k]는 a[k], a[k+1] ... a[n-1]중 가장 최소값이므로 x > n-1이면 a[k] < a[x]이다
∴ invariant 성립
(3) Result : invariant가 성립한다
Recursive selection sort
int sort(int a[], int n){
int j, m, t;
m = 0;
for(j = 0; j <n; i++){
if(a[m]>a[j]) m = j;
}
t = a[0]; a[0] = a[m]; a[m] = t; //여기서 a[0] 해결
sort(a+1, n-1);
return ;
}
proof of invariant
invariant : sort가 성공한다 (함수가 k번 실행된다)
- a[0] < a[1] < ... < a[k-1]을 만족한다
- a[k-1] < a[x] if x > k-1을 만족한다
(1) base : P(1) 일 때, a[0]에는 전체 배열 중에서 최솟값이 오게 됨 → a[0]이 가장 작고, 모든 x는 a[0]보다 크다
∴ invariant 성립
(2) Step : n-1일 때 sort가 성공한다면(→P(n-1)),n일때 sort가 성공함(→P(n))
재귀 호출이 끝난 후 (P(n-1)) : a[1] < ... a[n-2]이라면
함수가 끝날 때 (P(n)) : a[0] < a[1] < .. < a[n-1]이 성립한다 * a[0]은 재귀에서 나오는 것이 아니라 a[0] 재귀에 들어가기 전에 나옴
재귀이기 때문에, 이전 값은 그대로 유지되고 그 후 가장 작은 숫자를 a[n-1]과 바꾸어준다.
따라서 a[n-1] < a[x]인 값은 모두 a[n-1] 뒤에 있으므로 x > n-1일 때 a[n-1] < a[x]이다.
∴ invariant 성립
(3) Result : sort가 성공적으로 실행된다.
The complexity
\(T(n) = n + T(n-1) = n + n-1 + T(n-2)...\)
\(T(n) = O(n^2)\)
'CS > Data Structure' 카테고리의 다른 글
[ Arrays for search, insert, delete ] Packed unsorted (2) | 2024.04.09 |
---|---|
Merge Sort (0) | 2024.04.09 |
Binary search (2) | 2024.03.29 |
Linear search (0) | 2024.03.26 |
수학적 귀납법과 명제 (4) | 2024.03.25 |