Invariant de boucle de la recherche linéaire

Dans le cas de recherche linéaire, la variante boucle sera la sauvegarde utilisée pour sauvegarder l'index(sortie) .

nommons le magasin de support comme index qui est initialement fixé à zéro.La variante de boucle doit être conforme à trois conditions :

• initialisation: cette condition est vraie pour la variable index.depuis, il contient zéro qui pourrait être un résultat et vrai avant la première itération.
• entretien : l'indice restera nul jusqu'à ce que le point v soit localisé. C'est également vrai avant l'itération et après la prochaine itération.Comme, il sera placé à l'intérieur de la boucle après la condition de comparaison réussit.
• Résiliation : indice de contenir zéro ou l'index du tableau de l'article v.

.

invariant de Boucle serait

avant chaque 0 <= i < k, où k est la valeur actuelle de la variable d'itération de boucle, A[i]!= v

Sur la boucle de résiliation:

si Un[k] == v, alors la boucle se termine et sorties k

si A[k]!= v, et k + 1 = = n (Taille de la liste) alors boucle se termine avec une valeur nulle

preuve de L'exactitude: laissé comme un exercice

LINEAR-SEARCH(A, ν)
1  for i = 1 to A.length
2      if A[i] == ν 
3          return i
4  return NIL 

invariant de boucle: au début de l' i ième itération de la for boucle (lignes 1-4),

∀ k ∈ [1, i) A[k] ≠ ν.  

Initialisation:

i == 1 ⟹ [1, i) == Ø ⟹ ∀ k ∈ Ø A[k] ≠ ν,

ce qui est vrai, que toute déclaration concernant l'ensemble vide est vrai (vides de sens, de vérité).

Entretien: supposons que l'invariant de boucle est vrai au début de l' i ième itération de la for boucle. Si A[i] == ν, le l'itération actuelle est la dernière (voir résiliation section), car la ligne 3 est exécutée; sinon, si A[i] ≠ ν nous avons

∀ k ∈ [1, i) A[k] ≠ ν and A[i] ≠ ν ⟺ ∀ k ∈ [1, i+1) A[k] ≠ ν,

ce qui signifie que la boucle invariante sera toujours vraie Au début de la prochaine itération (le i+1 th).

résiliation:for boucle peut-end pour deux raisons:

1. return i (ligne 3), si A[i] == ν;

2. i == A.length + 1 (dernier test du for boucle), auquel cas nous sommes au début de la A.length + 1ème itération, donc l'invariant de boucle est

   ∀ k ∈ [1, A.length + 1) A[k] ≠ ν ⟺ ∀ k ∈ [1, A.length] A[k] ≠ ν
   

   et NIL valeur est retournée (ligne 4).

Dans les deux cas, LINEAR-SEARCH se termine comme prévu.

l'algorithme LS que j'ai écrit est-

LINEARSEARCH(A, v)
  for i=0 to A.length-1
    if(A[i] == v)
      return i
  return NIL

j'ai fait mes propres hypothèses pour l'invariant de boucle pour vérifier l'exactitude de la recherche linéaire..... Peut-être que c'est totalement faux donc j'ai besoin de suggestions sur mes suppositions.

1) à L'Initialisation - à i = 0, nous recherchons v à i = 0.

2) aux itérations successives - nous recherchons V till i < A. length-1

3) à la fin-i = A. length and till A. length we kept looking for v.

L'invariant pour la recherche linéaire est que chaque élément avant que je n'est pas égal à la clé de recherche. Un invariant raisonnable pour la recherche binaire pourrait être pour une gamme [faible, élevé), chaque élément avant faible est moins que la clé et chaque élément après élevé est plus grand ou égal. Notez qu'il y a quelques variations de la recherche binaire avec des invariants et des propriétés légèrement différentes - c'est l'invariant pour une recherche binaire "inférieure" qui renvoie l'indice le plus bas de tout élément égal à ou supérieures à la clé.

Source:https://www.reddit.com/r/compsci/comments/wvyvs/what_is_a_loop_invariant_for_linear_search/

me semble correct.

supposons que vous avez un tableau de longueur i, indexé à partir de [0...i-1], et l'algorithme vérifie si v est présent dans ce tableau. Je ne suis pas totalement sûr, mais je pense, l'invariant de boucle est comme suit: si j est l'indice de v, alors [0..j-1] est un tableau qui n'ont pas de c.

initialisation: avant itération à partir de 0..i-1, le tableau courant coché (none), ne se compose pas de v.

Maintenance : Sur la recherche de la v j, tableau de [0..j-1] un tableau sans v.

terminaison: comme la boucle se termine à la découverte de v à j, [0..j-1] est un tableau sans j.

si le tableau lui-même n'a pas v, alors j = i-1, et les conditions ci-dessus seront toujours vraies.