Как определить инвариант цикла?

Question

Мы знаем, что вариант цикла определяется как оператор, который является истинным до и после каждой итерации цикла. Но слишком ли это определение? Давайте посмотрим на конкретный пример: линейный поиск.

Входной сигнал: Последовательность п чисел А = (а , A , A , ..., а _п) и значение v

Выход: индекс я такая, что v = A [я] или NIL, если v не найден в

Вот мой псевдокод:

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

Так типичный (так как мы ищем слева направо) v не находится в левой части текущего индекса или математически P: ∀p ∈ {1, 2, ..., i - 1}, A[p] ≠ v. Это явно верно даже в начале, потому что p ∈ Ø ложно, что делает P true, помня, что каждый универсально квантифицированный оператор можно рассматривать как условное утверждение. (Но об этом говорить неформально: в начале нет ничего с левой стороны v.)

Мы также можем использовать условное утверждение, которое является менее ограничивающим. В этом случае Q: If A[i] = v, then 1 ≤ i ≤ n. Очевидно, что это верно, если v найдено. Если v не найдено, A [i] = v является ложным, а Q становится истинным независимо от значения i. Q также верно, если мы изменим наш алгоритм на поиск справа налево.

Возможно, мы хотим быть менее ограничивающими. Как насчет использования утверждения, которое всегда верно? 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. Так как это было верно для г = п, если функция возвращает NIL, то есть

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

Ваш кандидат P является полезным для этой цели, и другие - нет.

Кроме того, вы не можете просто выбрать инвариант цикла - вам нужно доказать это, чтобы доказать правильность вашего алгоритма. Итеративный характер циклов подкрепляется доказательством по индукции, и инварианты, подобные вашему кандидату P, легко доказать таким образом.