컨텐츠 바로가기

Loop Invariant (ex. 삽입정렬[java로 구현])

http://kuphy00.egloos.com/2475164

오늘은 Loop 불변성에대해 이야기를 해보고자 한다.

알고리즘 입문시 제일 먼저 나온다. 알고리즘 정복이라는 목표를 갖고 도전을 하지만...
첫 판부터 도무지 몬소리인지 못알아 들어 심히 괴롭다.
아마 미실이라면 이렇게 말할꺼다."이번엔 우리가 졌습니다."라고...

나또한 질뻔했지만, 좀 생각해보니 정리가 되는듯 싶어 나름데로 또 적어본다.
아마 이글을 봐도 헷갈릴수도 있는건 아마 내가 생각나는데로 글을 작성했기 때문이 아닐까....싶다.

암튼 그럼 쭉쭉~~써나가보자.

loop invariant 란 루프를 돌 동안 유지되어야 하는 statement  이다.

Loop invariant 를 통해 Loop가 완성적인지 아닌지 체크해 볼 수 있으므로,루프를 이용한 알고리즘을 짤때 로직 점검에 아주 탁월한 방법이다.


Loop invariant를 증명해 보이려면 세가지 성질을 만족해야한다.

1. 초기조건(Initialization)
 루프에 처음들어갈때 변수의 변화 및 statement(조건)의 변화가 맞는지 판단해서, 루프에 정확하게 들어가는지 확인한다.

2. 유지조건(Maintenance)

루프가 시작하기전부터해서, 다음 루프로 넘어가기 전까지 만족해야 되는 조건으로 이 조건이 알고리즘의 목적에 부합하는지를 판단한다.

3. 종료조건(Termination)
루프가 끝났을때, 우리는 사용가능하고 유용한 결과를 얻어야 하며, 이것이 문제해결(알고리즘의 목표)에 도움이 되는 결과가 나오는지 확인한다.

삽입정렬의 예시(알고리즘 의사코드가 아닌 JAVA 소스를 직접 썻다 그나마 이해가 좀 가라고..ㅋㅋ)

  int A[] = {5,2,4,6,1,3};
  System.out.print("정렬전==>");
  for(int y=0;y<A.length;y++){
       System.out.print(A[y]+",");
  }
  System.out.println();
  for(int j=1 ;j<A.length ; j++){
       int key = A[j];
       int i=j-1;
       while(i >= 0 && A[i]>key ){
            A[i+1] = A[i];
            i=i-1;
       }
       A[i+1] = key;
  }
  System.out.print("정렬후==>");
  for(int x=0 ; x<A.length ; x++){
       System.out.print(A[x]+",");
  }

우선 이로직의 핵심부터 보자.

for문에서
1. 내부로직은 배열 A에서 index가j 이전의 원소들은 정렬이 되어있어야만 한다.(이래서 j의 초기값 설정이 중요하다.)
2. 현재 추출한 A[j]을 이전 원소들(모두 비교할 필요는 없다 그래서 wile문을 쓴거다)과 크기를 비교해서 적당한 위치를 찾아 배열에 삽입하면 끝이다. for 문 내부를 수행하고 나면 결국 배열 A의 index j까지도 정렬되어있다.

고롬 Loop invariant<=요건 뭐냐?
위의 로직이 맞느냐를 증명하겠다는 건데
1. for문을 돌릴때 초기값 설정을 잘했는가?(예가 for문이어서 for문이라고 적었지 엄밀히 말하면 loop이다.)
2. for문을 돌리는 동안 j가 증가하는데 그 증가할때마다 로직이 잘 맞아들었느냐?
3. for문을 나올때 정확한 시점에 잘 나왔느나?

요걸 보면 로직이 증명이 되었다는 뭐..그런 거다ㅏ.

그럼 보자...

Initialization : j=1 에 대해서, A[0...j-1] = A[0] 이 정렬된다.
==>배열의 인덱스 1이전의 배열(여기서는 원소가 A[0] 밖에 없는 배열이다.)이 정렬되어있는가? 원소가 하나밖에 없으니 당근 정렬되어있다.

Maintenance : j가 증가하고 그에따라 A[0...j]가 정렬된다.
==>j가 초기값에서 1만큼 증가했을때 내부 로직을 수행하고 나면 index j-1까지는 정렬되어있다.
(wile문을 통해서 앞의 원소들과 비교해서 적당한 위치를 찾아 삽입하는 로직이 있다. 이로직이 끝나면 정렬되어있다는 것이다.)

Termination : j < length[A] 일때 루프는 끝이나며, 루프가 끝이 났을때는 A[0...j] 은 정렬이 끝나있다.

==>Maintenance 내용을 심히 생각해보면 for문 내부 로직은 index j 까지는 정렬을 해준다는 것이다.
따라서 우리의 목적은 배열의 정렬은 배열의 갯수까지만(length[A]일때는 배열의 인덱스는 length[A]-1이다.) loop 를 수행하면 되니깐, loop 탈출 조건(j < length[A])즉, 배열의 인덱스 j= length[A]-1까지는 정렬이 되어있다는 소리이고 그 이후에는 loop문을 나오는 것이 맞다.(즉, 적당한시기에 잘 빠져나왔다.)


오늘은 여기까지...휴...


Ref. http://en.wikipedia.org/wiki/Loop_invariant
Intorduction To Algorithms by Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, Clifford Stein


덧글|덧글 쓰기|신고