루프 불변성을 어떻게 정의합니까?

Question

루프 변형은 루프의 모든 반복 전후에 true 인 문으로 정의됩니다. 그러나 그 정의가 너무 느슨한가? 구체적인 예를 살펴 보겠습니다 : 선형 검색.

입력 : 인덱스 : N 번호 A = (a ₁하는 ₂하는 ₃ ...하는 N) 및 V 값

출력의 순서 그래서 일반적인

linear_search(A, v) 
1 for i ∈ {1, 2, ..., n} 
2  if A[i] = v 
3   return i 
4 return NIL 

: 내가되도록 V는 V = A 여기서

에서 발견되지 않으면 [I] 또는 NIL 내 의사 인 루프 불변량은 (왼쪽에서 오른쪽으로 검색하기 때문에) v가 현재 색인의 왼쪽에 있지 않거나 수학적으로 P: ∀p ∈ {1, 2, ..., i - 1}, A[p] ≠ v.입니다. p Ø Ø가 false이기 때문에 시작시에도 분명히 사실입니다. 그러면 P 사실, 모든 보편적으로 정량화 된 문장은 조건문으로 생각할 수 있습니다. (그러나 비공식적으로 생각하는 것이 더 쉽습니다. 처음에는 v의 왼쪽에 아무것도 없습니다.)

제한이 적은 조건문을 사용할 수도 있습니다. 이 경우, Q: If A[i] = v, then 1 ≤ i ≤ n. 분명히 v가 발견되면 이것은 사실입니다. v가 발견되지 않으면, A [i] = v는 거짓이고 Q는 i의 값에 관계없이 참이됩니다. 알고리즘을 오른쪽에서 왼쪽으로 검색하도록 변경하면 Q가 true입니다.

어쩌면 우리는 그보다 덜 제한되기를 원할 것입니다. 항상 진실한 진술을 사용하는 것은 어떻습니까? R: Either A[i] = v or A[i] ≠ v. 루프의 반복마다 전후에 R이 유지됩니다.

P, Q 및 R 문 중 루프 불변으로 사용할 수있는 문장은 어느 것입니까?

Answer 1

루프 불변의 문자는 무엇입니까 에을 입력 하시겠습니까?

linear_search(A,v) = i ⇒ A[i] = v 

및

linear_search(A,v) = NIL ⇒ v ∉ A 

첫 번째는 간단합니다 : 어쩌면 당신은, 알고리즘 즉, 정확하다는 것을 증명하고 싶다. 두 번째를 증명하기 위해, 당신은 내가 대한 사실 때문에 루프 불변 P.를 사용할 수있다 = N 함수가 NIL을 반환하는 경우, 당신은

linear_search(A,v) = NIL 
⇒ ∀p ∈ {1, 2, ..., n}, A[p] ≠ v 
⇒ v ∉ A 

후보자 P는이 목적을 위해 유용 가지고 있고, 다른 사람들은 그렇지 않습니다.

또한 루프 불변성을 선택할 수는 없으며 알고리즘이 올바른지 증명해야합니다. 루프의 반복적 성격은 유도에 의한 증명에 도움이되며, 후보자 P와 같은 불변량은 그렇게 쉽게 증명할 수 있습니다.