루프 불변성

루프 불변성이란?

반복문이 실행되는 동안 항상 참이 되는 조건이나 성질

루프 불변성의 특징

1. 초기 조건 (Initialization): 반복이 시작될 때 불변성이 참이어야 함
2. 유지 조건 (Maintenance): 루프의 각 단계에서 불변성이 참이어야 함
3. 종료 조건 (Termination): 루프가 종료될 때 우리가 원하는 솔루션을 얻을 수 있어야 함

예시

삽입정렬

INSERTION-SORT(A, n)

for i = 2 to n
      key = A[i]
      j = i - 1
      while j > 0 and A[j] > key
            A[j + 1] = A[j]
            j = j - 1
      A[j + 1] = key

루프 불변성 : A[1 : i - 1]은 정렬된 상태이다.

• 초기조건
  • i = 2 부터 시작
  • A[1 : 2] 의 요소는 한 개 뿐이므로, 이미 정렬된 상태
• 유지조건
  • A[i]를 적절한 위치에 삽입
  • 루프가 실행되면 A[1 : i] 까지 정렬된 상태를 유지
  • 이후 A[1 : i + 1] 까지 정렬된 상태를 유지
• 종료조건
  • 루프가 n까지 실행될 때 n은 리스트 A의 길이.
  • 이때, A[1 : n] 까지 정렬된 상태가 됨

삽입 정렬의 루프 불변성이 성립하며, 알고리즘이 정확함

Sum Array 함수

SUM-ARRAY(A, n)

sum = 0
for i = 1 to n
      sum = sum + A[i]
return sum

루프 불변성 : Sum은 배열 i까지의 합이어야 한다.

• 초기조건
  • 처음 시작시 sum은 0으로 초기화 됨.
  • 0개의 요소의 합은 0이다.
• 유지조건
  • 루프마다 A[i]를 sum에 더해주면서 sum은 i까지의 합
• 종료조건
  • i = n + 1 이 되면 루프 종료
  • 이때, sum은 A의 n개의 모든 합을 나타냄

SUM ARRAY 함수의 루프 불변성이 성립하며, 알고리즘이 정확함