Это правильный инвариант для этого цикла?

Question

Это псевдокод для линейного поиска в массиве, возвращающего индекс i если желаемый элемент e в массиве A найден, NIL в противном случае (это из книги CLRS, 3-е издание, упражнение 2.1-3):

LINEAR_SEARCH (A, e)
    for i = 1 to A.length
        if A[i] == e
            return i
    return NIL

Я пытаюсь экстраполировать цикл, инвариантный от него, поэтому, в соответствии с моим пониманием, я думаю, что он представлен тем, что в любой данный момент в цикле подмассив A[1..i-1] содержит только те значения, для которых проверка на равенство оказывается ложной.

В частности, перед первой итерацией i-1 == 0 что подразумевает, что длина подмассива равна нулю, поэтому не может быть элемента v принадлежащий ему так, что v == e, Перед любой следующей итерацией, являющейся также тестом на равенство и выходным условием, предполагаемое свойство инварианта должно оставаться истинным, иначе цикл уже завершился бы. По окончании это либо то, что функция собирается вернуть индекс (и в этом случае инвариант цикла является тривиально истинным), либо возвращение NIL (в этом случае i == A.length + 1Таким образом, инвариант цикла выполняется для любого 1 < j < i).

Это правильно? Не могли бы вы предоставить правильный инвариант цикла, если это не так?

Спасибо за внимание.

Answer 1

• Инвариант цикла: в начале каждой итерации цикла for мы имеем A[j] != e для всех j < i,

• Инициализация: до первой итерации цикла выполняется инвариант, поскольку массив пуст.

• Обслуживание: инвариант цикла поддерживается на каждой итерации, так как в противном случае на i-я итерация есть некоторые j < i такой, что A[j] == e, Однако в этом случае для j-я итерация цикла значение j возвращается, а нет i-я итерация цикла, противоречие.

• Завершение Когда цикл завершается, может быть два случая: во-первых, он завершается после i <= A.length итерации и возвраты iв этом случае if условно гарантирует, что A[i] == e, Другой случай заключается в том, что i превышает A.length, в этом случае по инварианту цикла мы имеем это для всех j <= A.length, A[j] != e, это возвращение NIL является правильным.