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

Имеется алгоритм линейного поиска
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 ∈ {}
  • Вопрос задан
  • 119 просмотров
Решения вопроса 1
dollar
@dollar
Делай добро и бросай его в воду.
1. A[i] ∈ A
2. i ∈ {0, ...A.length - 1} или i ∈ {}

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

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

Войдите, чтобы написать ответ

Войти через центр авторизации
Похожие вопросы