Инвариант в линейном поиске?

Question

[Дмитрий]

Имеется алгоритм линейного поиска

A = {1, 2, 7, 5, 8}
v = 7

def search(A, v)
    i = 0
    while i < A.length do
        if A[i] == v then
            return i
        end
        i++
    od
    return nil
end

A - набор элементов
i - индекс текущего элемента
v - элемент, который мы ищем

Верно ли, что инвариантом будет:
1. A[i] ∈ A
2. i ∈ {0, ...A.length - 1} или i ∈ {}

Answer 1

[dollar]

1. A[i] ∈ A
2. i ∈ {0, ...A.length - 1} или i ∈ {}

Как по мне, такой инвариант будет несколько бесполезен, поскольку не позволяет доказать правильность алгоритма (по индукции). Также "или i ∈ {}" ещё более бесполезное дополнение к условию, поскольку, хоть и не делает инвариант неверным, но делает его слабее, ведь внутри цикла (да и после него) в i всегда какое-то число.

Имхо, хороший инвариант:
В элементах A с индексами до [i-1] включительно не содержится v.