(+- Recursive) Binary Search 증명

1. Binary Search 증명 

[Proof by Loop Invariant]

가설 : a[i] = x인 i가 있다면, l <= i <= r 이다. 

 

- 초기 (Init) (최초에 성립한다) : l = 0, r = n - 1인 상황이다. a[i]가 존재한다면, l 또는 r 너머에 있을 상황은 존재하지 않는다. 

- 중간 (meintance) (Invariant를 깰 상황, 코드가 전혀 없다.) 

: if ( x < a[mid] ) : mid 이후는 a[i]가 없음이 보장. mid가 r이 된다.

if (x > a[mid) : 반대

>> l과 r이 변해도, l <= i <= r인 invariant는 깨지지 않는다. 여전히 항상 성립한다. 

 

- 끝 종료 (terminate) : 존재하면 idx, 존재하지 않으면 -1을 반환한다. 

else // x == a[mid] : (종료함으로서 search를 성공했으며, 종료하는 과정에서도 invariant는 깨지지 않았다. 

 

2. Recursive Binary Search 증명

[Proof by Induction]

가설 : 만약 어떤 i에 대해서 a[i] = x라면, 이 함수는 i를 반환한다. 

 

Base : n = 0인 경우, "어떤 i에 대해서 a[i] = x" 가 성립할 방법이 없고, 함수는 -1을 리턴한다.

Step :

search(a, mid-1, x)에서 성립한다면 -> search(a, n, x)에서도 성립한다. 

Case 1. a[m] = x인 경우, 

Case 2. a[m] > x인 경우, 답은 0, 1, ... , mid에 있는 것을 알 수 있다. search(a, mid - 1, x)가 참임이 보장되므로 우리는 a[i]=x라면 i를 리턴할 수 있다. 

Case 3. 2와 비슷