이 루프가 일정하지 않습니까?

Question

선형 검색 루프에 대한 의사 :

for j = 1 to A.length 
    if(A[j] = v) 
     return j; 
return NIL 

루프 내가 작성한 불변 :

루프의 각 반복의 시작에서, J 후 다음 인덱스 여기서, A [j-1]은 v과 동일하지 않습니다.

초기화 :

J이 에 해당하고 작은 것보다 A.length 여부를 확인하기 전에, 이전 인덱스가 입니다. 그런 다음 A [0]이 존재하지 않기 때문에 A [0]은 v과 같지 않습니다.

유지 :

A가 [j]가 V 는 다음 루프가 종료 같으면. 우리는 다음 반복을하지 않는다는 것을 의미합니다. 그러나 v과 같지 않으면 루프의 다음 반복이 실행되고 루프 불변성이 유지됩니다.

종단 :

조건의 종료 for 루프 J는 V는 A [J] 동일하거나보다 큰 A.length 것이 원인이다. 1하여 각 루프 반복 증가 J 때문에, 우리는이 J 까지 V A.length 대해보다 큰 인 모든 요소를 ​​확인 하였다. 따라서 알고리즘은 정확합니다. v이 A [j]과 같으면 우리가 검색해 온 요소를 찾은 것입니다. 따라서 알고리즘은 정확합니다.

이 정보가 맞습니까?

Answer 1

너무 나쁘지는 않지만 약간 개선 할 수 있습니다.

루프 불변 : "next after where ..."언어가 어색하고 알고리즘이 정확하다는 증거로 사용하지 않으므로이를 유지할 이유가 없습니다. 이와 같은 것이 더 좋을 것입니다. "각 반복의 시작 부분에 A [i] == v가되도록 i가 존재하지 않습니다.

유지 보수 : A [j]! = v 인 경우 루프가 계속됩니다. A [i] == v 및 A [j]!와 같은 i < j가 없기 때문에 루프가 계속됩니다!= v이면 A [i] == v가되도록 i < = j이 존재하지 않으며 루프 불변 값은 j의 다음 큰 값을 유지합니다.

그런 다음 종료 조건에서 사용할 수 있습니다. 배열에서 v가 발견되면 루프가 일찍 끝나고 인덱스가 반환됩니다. 그렇지 않으면, 루프 불변 값은 j == length + 1에 대해 유지되고, A [i] == v가되도록 임의의 i가 존재하지 않는다는 것, 즉 v가 배열에서 발생하지 않는다는 것이 알려져있다.