Loop Invariant 루프 불변성 (feat. Insertion Sort)

루프 불변성은 알고리즘이 올바른지 증명하는데 사용된다.

Loop invariant 증명을 위한 Insertion Sort Pseudocode

 

 

 

1. Initialization(초기화) : 첫 번째 루프 반복 전에 루프 불변량이 유지된다는 것을 보여준다
   1. j=2의 경우 해당배열(하위배열)은 A[1] 단일 element로 정렬되어있다고 볼 수 있다.
2. Maintenance(유지) : 각 반복이 루프 불변성을 유지한다는 것을 보여준다.
   1. A[1.. j] 하위배열이 정렬되어있음
3. Termination(종료) : 루프가 종료되면 불변량은 알고리즘이 정확하다는 것을 보여주는 데 도움이 되는 유용한 속성을 제공한다.
   1. 루프 종료 조건은 j > A.length (=n), j = n-1
   2. 하위 배열 A[1..n]가 전체 배열이라는 것을 관찰하면 전체 배열이 정렬되었다고 결론을 내린다.
   3. 따라서, 알고리즘은 정확하다.

 

• loop invariant is true prior to every iteration of the loop( 1, 2 속성으로 루프의 모든 반복전에 참이다 )
• 3번째 속성이 알고리즘의 정확성을 보여줌