Proof by invariant

int search(int a[], int n, int x)
{
	int l, r, m;
	l = 0;
	r = n - 1;
	while (l <= r)
	{
		m = (l + r) / 2;
		if (x = a[m])
			return m;
		else (x < a[m])
			r = m - 1;
		else
			l = m + 1;
	}
	return -1;
}

배열의 왼쪽 끝은 l 이 가리키고있고 오른쪽 끝은 r이 가리키고 중간을 m이 가리킴

찾아서 리턴할때 l,r안변하지

x < a[m] 일때 소팅되어있기 때문에 저 조건을 깰 방법이 없음

Invariant: 만약 어떤 i에 대해 a[i] = x 라면 l ≤ i ≤ r 이 항상 성립한다

• invariant 는 최초에 성립하고, 코드가 진행되며 invariant가 깨질수있는 상황이 전혀 없다

한번 루프 돌때마다 r - l 이 줄어들어.

그러나 한없이 줄어들수는 없음. 언젠가는 l ≤ r조건이 깨지게됨

!(l ≤ r) < = > l >r 인데 이게 설=ㅇ립할리가 없음

• a[i] = x 인 i가 없다면 루프는 반드시 끝나고 -1이 리턴됨
• a[i] = x 인 i가 있다면 루프안에서 반드시 리턴됨

내가 생각하는 논리가 완결성있다는걸 증명하는게 중요해

recursive Binary search v1

int search(int a[], int n, int x)
{
	if (n == 0)
		return -1;
	if (n == 1)
	{
		if (a[0] == x)
			return 0;
		else
			return -1;
	} // 길이가 0, 1 일때의 경우 처리-> 생각해보면 1일때는 밑에경우에도 처리가능함
	// 나머지경우 처리해보자
	int m = n / 2;
	if (a[m] == x)
		return m;
	else if (x < a[m])
		return search(a, m, x);
	else
	{
		int result = search(a + m + 1, n - (m + 1), x);
		if (result == -1)
			return -1;
		else
			return result + m + 1;
}