Правильность алгоритма

Question

Я изучаю инварианты цикла в настоящий момент, и у меня возникают проблемы с моим выбором для инварианта для алгоритма линейного поиска.

Inpput: A[1 ... n] of integers, k an integer value 
Output: true if k belongs to A[1 ... n] false otherwise 

LSearch(A,k) 
i := 1 
found := false 
WHILE i<=n AND found=false DO 
    IF A[i] = k THEN 
    found := true 
    i:=i+1 
return found 

Утверждение, которое я выбираю это:

• найдено содержит истинным или ложным, если к присутствует среди [1] и A [I]
  

Перед тем, первая итерация выполняется, потому что в то время в A [1] находится один элемент и найденный инициализируется как false.

После цикла i может быть равным i: = 1 найдено: = falseto n и/или найдено может быть истинным (пока условие), поэтому утверждение остается неизменным с учетом i < = n.
Считаете ли вы, что это может быть правильно?

Answer 1

Утверждение верно, но также и бесполезно. found является логическим и будет содержать True или False, независимо от свойств A. Это не поможет вам доказать правильность вашего алгоритма.

Был ли этот вопрос с множественным выбором? Каковы были другие варианты?