Sortings

• Insertion sort, merge sort, quick sort 등의 다양한 정렬 알고리즘들이 있다.

Insertion Sort

• Incremental algorithm이다.
• 앞의 원소부터 차례대로 증가하며 체크한다.

그렇다면, 이 알고리즘 방식이 정말로 내가 원하는대로 정렬해주는가?

---

Loop Invariants

• 어떤 알고리즘이 주어졌을 때, 왜 이 알고리즘의 correctess를 보이기 위해 사용하는 방식
• 루프가 반복되는 동안 항상 유지되는 성질
  Initialization
  - It is true prior to the first iteration of the loop.
  Maintenance
  - If it is true before an iteration of the loop, it remains true before the next iteration.
  Termination
  - When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.

Insertion sort를 통해 Loop Invariant를 활용한 correctness 증명을 적용해보자.

---

Insertion Sort에서의 Loop invariant

At the start of the loop, the subarray A[1...j-1] consists of the elements originally in A[1...j-1] but in ascending order.

Initialization

• 첫 반복 전에 j는 2이다. 이를 loop invariant에 대입해보자.
  • At the start of the loop, A[1...1] consists of the elements originally in A[1..1] but in ascending order.
    -> 참

Maintenance

• Maintenance에서 보여야 하는 성질의 핵심은 아래와 같다.
  • 루프 실행 전에도 참이라면, 다음 루프 실행 전에도 참이어야 한다.
    -> 루프 실행 전에도 Loop invariant를 만족한다면, 다음 루프 실행 전에도 이 Loop invariant를 만족해야 한다.
• 그러므로, 루프 실행 전에 Loop invariant를 만족한다고 하자.
  • At the start of the j-th iteration of the loop, A[1...j-1] consists of the elements originally in A[1...j-1] but in ascending order.
• A[1...j-1]를 j까지로 확장하는 것이다.
  • 변수 i를 통해 A[j-1]부터 A[1]까지 순회하며 A[j]보다 큰 원소들을 오른쪽으로 옮긴다. 해당 과정이 멈춘 경우, A[j]는 멈춘 위치 +1인 곳(i+1)에 삽입된다. 따라서 정렬된 A[1...j-1]의 배열에 key를 올바른 위치에 삽입한다. 즉, 삽입된 위치에는 A[j]가 있고, A[j] 기준으로 왼쪽은 A[j]보다 작거나 같은 값들, 오른쪽은 A[j]보다 큰 값들이 존재하므로 기존 배열의 정렬성을 해치지 않고 올바르게 삽입된다.
• 이제, j를 증가시켜서 A[1...j]로 만들면, 이 배열은 다음 iteration 시작 시에도 정렬된 상태이므로 Loop Invariant가 유지된다.
  -> 따라서 Maintenance 역시 참이다.

Termination

• for loop이 종료되었을 때 j = n + 1이다.
• 이 j 값을 loop invariant에 넣어보자.
  • A[1...n] consists of the elements originally in A[1...j] but in ascending order.
    -> correctness 증명 완료.