Loop invariant

K PizzaCola·2021년 6월 9일

Algorithms

Datastructure and algorithms

목록 보기

1/7

개요

알고리즘에서, 반복문을 실행하면서 변하지 않는 부분
ex) 삽입 정렬에서 k번째 정렬을 실행할 때, k - 1개는 미리 정렬되어 있는 특성

알고리즘 검증

Step 0

print(), debug로 출력이나 프로그램 상태를 확인한다.

Step 1

assert로 조건을 입력한다.

Step 2

입력 개수, 출력 개수, 수행 시간, 시간 복잡도 등 확인

Step 3

시작 조건 (Precondition, Q)
Loop invariant (P)
- 시작 조건과 종료 조건 사이에 반복문에서 성립하는 상황 / 조건 등등
- 루프를 진행하는 동안 알고리즘이 정확하게 동작하고 있는가?
- 알고리즘이 올바르게 종료 조건을 향해 가고 있는가?
- 알고리즘을 지정된 시간 안에 종료할 수 있는가?
종료 조건 (Postcondition R)

일반적인 알고리즘 구조

초기화 : {Q}와 {P}가 참
진행 : P 와 B가 참
종료 : P & !B가 참이며, R이 참

Ex1) Pow(a, b) 구현

pow(a: int, b: int):
    x = a
    y = b
    z = 1
    while y > 0:
        z = z * x
        y = y - 1
    return z

여기서 시작조건 Q는 x = a, y = b, z = 1이다.

Loop invariant는 k번째 루프를 시작하기 전에

z = a ^ k

를 만족한다.

만약 z = 0이었다면, Loop invariant에서 z가 언제나 0이므로, 만족하지 않는다.

Ex2) m에서 n까지 합

sum(m: int, n: int):
    z = 0
    k = m
    while k <= n:
        z = z + k
        k = k + 1
    return z

precondition Q는 $m <= n$ 이다
branch condition B 는 $k <= n$ 이다.
Loop invariant는 $k$ 에 대한 루프가 동작할 때, $z$ 에는 $[m, k-1]$ 의 합을 가지고 있는 것이다. ( $k$ 는 $m <= k < n$ 이다.)
postcondition R은 $z = [m, n]$ 까지 합

Ex3) 음수 양수 분리하기

arrange(a: List(int)):
    h = 0
    j = len(a) - 1
    while h < j:
        if a[h] <= 0:
            h = h + 1
        else:
            a[h], a[j] = a[j], a[h]
            j = j - 1
    
    return a

시작 조건 Q : 배열이 있다, $h = 0, j = len(a) - 1$
분기 조건 B : $h < j$
Loop invariant P : 음수는 배열 왼쪽, 양수는 배열 오른쪽으로 이동한다. 그래서 k번째 반복문이 시작할 때는 k개의 숫자가 우리가 원하는 위치에 있다.
종료 조건 R : h를 기준으로, 왼쪽에는 음수, 오른쪽에는 양수가 있다.