Инвариант цикла линейного поиска

После того, как вы просмотрели индекс i и еще не нашли v, что вы можете сказать о v в отношении части массива до i и в отношении части массива после i?

LINEAR-SEARCH(A, ν)
1  for i = 1 to A.length
2      if A[i] == ν 
3          return i
4  return NIL 

Инвариант цикла: в начале iй итерации for цикла (строки 1–4),

∀ k ∈ [1, i) A[k] ≠ ν.  

Инициализация:

i == 1 ⟹ [1, i) == Ø ⟹ ∀ k ∈ Ø A[k] ≠ ν,

что верно, как верно любое утверждение о пустом множестве (бессодержательная истина).

Обслуживание: предположим, что инвариант цикла истинен в начале i-й итерации for-го цикла. Если A[i] == ν, текущая итерация является последней (см. раздел завершение), так как выполняется строка 3; иначе, если A[i] ≠ ν, имеем

∀ k ∈ [1, i) A[k] ≠ ν and A[i] ≠ ν ⟺ ∀ k ∈ [1, i+1) A[k] ≠ ν,

это означает, что инвариантный цикл все еще будет истинным в начале следующей итерации (i+1th).

Завершение: цикл for может завершиться по двум причинам:

1. return i (строка 3), если A[i] == ν;

2. i == A.length + 1 (последний тест цикла for), и в этом случае мы находимся в начале A.length + 1й итерации, поэтому инвариант цикла равен

   ∀ k ∈ [1, A.length + 1) A[k] ≠ ν ⟺ ∀ k ∈ [1, A.length] A[k] ≠ ν
   

   и возвращается значение NIL (строка 4).

В обоих случаях LINEAR-SEARCH заканчивается, как и ожидалось.

В случае линейного поиска вариантом цикла будет резервное хранилище, используемое для сохранения index(output) .

Давайте назовем резервное хранилище как index, для которого изначально установлено значение NIL. Вариант цикла должен соответствовать трем условиям:

• Инициализация: это условие выполняется для индексной переменной, поскольку оно содержит NIL, что может быть результатом и истинным до первой итерации.
• Обслуживание: индекс будет содержать NIL до тех пор, пока элемент v не будет найден. Это также верно до итерации и после следующей итерации. Так как она будет установлена ​​внутри цикла после успешного выполнения условия сравнения.
• Завершение: индекс будет содержать NIL или индекс массива элемента v.

.

Инвариант цикла будет

forevery 0 ‹= i ‹ k, где k — текущее значение переменной итерации цикла, A[i] != v

При завершении цикла:

если A[k] == v, то цикл завершается и выводит k

если A[k] != v и k + 1 == n (размер списка), то цикл завершается со значением nil

Доказательство правильности: оставлено в качестве упражнения

Предположим, что у вас есть массив длины i, проиндексированный от [0...i-1], и алгоритм проверяет, присутствует ли v в этом массиве. Я не совсем уверен, но думаю, что инвариант цикла выглядит следующим образом: Если j является индексом v, то [0..j-1] будет массивом, в котором нет v.