어떻게 하는거임
Introduction to Algorithms 연습문제 2.1-3 인데 -_- 증명에서 gg

다음의 검색문제를 생각해보자.
입력 : n개 수들의 수열 A=<a1,a2,...,an>과 어떤 값v
출력 : v=A[i]를 만족하는 인덱스 i. 만약, v가 배열 A에 존재하지 않을 경우에는 특수한 값 NIL
수열을 읽어보고 v의 값을 찾아보는 선형검색 의사코드를 작성하고, 루프 불변성을 이용해서 그 알고리즘이 타당함을 증명하라. 루프불변성의 세가지 필요조건을 충족하는지 반드시 확인해야 한다.

해서 아래 코드는 생각해냈거든요.

LINEAR_SEARCH(A,v)
   for i <- 1 to length[A] do
       if A[i]=v then
           return i
       end if
   end for
   return NIL
end

그런데 루프불변성 증명은 못하겠네요.

루프불변 : A[1..i-1] 안에는 v와 일치하는 값이 없다.
초기조건 : i=1일때, A[1..i-1]=A[1..0]안에는 아무것도 없으니 v와 값이 일치하지 않는다.
유지조건 : i=2,3,...,n일때, A[1..i-1] 안에는 v와 일치하는 값이 없으니까 A[i]까지 넘어왔다.
종료조건 : 종료되면서 i를 내뱉을때에는, A[1..i-1]안에 v랑 일치하는게 없다가 A[i]에서 일치하니 i를 내뱉고
　　　　   종료되며 NIL을 내뱉을땐 i가 n+1이니까 A[1..n]안에 v랑 일치하는게 없으니 NIL을 뱉은거다.

이렇게 하면 몇점? 30점?