Является ли этот цикл инвариантным правильным?

Question

псевдокод для линейного поиска цикла:

for j = 1 to A.length 
    if(A[j] = v) 
     return j; 
return NIL 

Loop инвариантного Я написал:

В начале каждой итерации для цикла, J является следующим индексом после где A [j-1] не соответствует v.

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

Когда J равна и перед проверкой, является ли он меньше, чем a.length, предыдущий индекс . Тогда A [0] не равно v, потому что в этом контексте A [0] даже не существует.

Обслуживание:

Если А [J] равна v, то цикл завершается. Это означает, что у нас нет следующей итерации. Но если он не равен v, тогда следующая итерация цикла выполняется при сохранении инварианта цикла.

Прекращение:

условия в результате чего цикл прекратить в том, что J больше, чем a.length или v равна A [J]. Поскольку каждый итерации цикла увеличивается J по , мы проверили каждые элементы против v до J больше, чем a.length. Следовательно, алгоритм правильный. Если v равно A [j], то это означает, что мы нашли элемент, который мы искали. Таким образом, алгоритм правильный.

Правильно ли это?

Answer 1

Неплохо, но вы можете внести некоторые улучшения.

Циклический инвариант: язык «следующий после того, где ...» неуклюжий, и вы не используете его в доказательстве правильности алгоритма, поэтому нет причин его поддерживать. Что-то вроде этого было бы лучше: «В начале каждой итерации не существует i < j таких, что A [i] == v".

Техническое обслуживание: цикл продолжается, если A [j]! = V. Так как не существует i < j таких, что A [i] == v и A [j]!= v, то также не существует i < = j, для которого A [i] == v, а инвариант цикла имеет место для следующего большего значения j.

Тогда вы можете использовать его в условии завершения: цикл заканчивается раньше, если он находит v в массиве и возвращает его индекс. В противном случае для j == length + 1 выполняется инвариант цикла, и известно, что i < = length не существует, так что A [i] == v, то есть v не встречается в массиве.