Comment définit-on un invariant de boucle?

Question

Nous savons qu'une variante de boucle est définie comme une déclaration qui est vraie avant et après chaque itération de la boucle. Mais cette définition est-elle trop vague? Regardons un exemple concret: la recherche linéaire.

entrée: Une séquence de n nombres A = (a 1 , un , un , ..., a n ) et une valeur v

sortie: un index i tel que v = a [i] ou NIL si v ne se trouve pas dans une

Voici mon pseudo:

linear_search(A, v) 
1 for i ∈ {1, 2, ..., n} 
2  if A[i] = v 
3   return i 
4 return NIL 

donc typique invariant de boucle serait que (puisque nous cherchons de gauche à droite) v n'est pas sur le côté gauche de l'index actuel, ou mathématiquement, P: ∀p ∈ {1, 2, ..., i - 1}, A[p] ≠ v. Ceci est clairement vrai, même au début, car p ∈ Ø est faux, ce qui rend P vrai, en se rappelant que toute déclaration universellement quantifiée peut être considérée comme une déclaration conditionnelle. (Mais il est plus facile d'y penser de façon informelle: au début, il n'y a rien du côté gauche de v.)

Nous pourrions également utiliser une instruction conditionnelle moins restrictive. Dans ce cas, Q: If A[i] = v, then 1 ≤ i ≤ n. Évidemment, ceci est vrai si v est trouvé. Si v n'est pas trouvé, A [i] = v est faux et Q devient vrai quelle que soit la valeur de i. Q est également vrai si nous changeons notre algorithme pour effectuer une recherche de droite à gauche. Peut-être que nous voulons être moins restrictifs que cela. Qu'en est-il de l'utilisation d'une déclaration qui est toujours vraie? R: Either A[i] = v or A[i] ≠ v. R tient avant et après chaque itération de la boucle.

Lesquelles des instructions P, Q et R sont valables pour être utilisées comme invariant de boucle?

Answer 1

Que voulez-vous un invariant de boucle pour? Peut-être que vous voulez prouver que votre algorithme est correct, à savoir que:

linear_search(A,v) = i ⇒ A[i] = v 

et

linear_search(A,v) = NIL ⇒ v ∉ A 

Le premier est facile. Pour prouver la seconde, vous pouvez utiliser votre invariant de boucle P. Comme il est vrai pour i = n si la fonction retourne NIL, vous avez

linear_search(A,v) = NIL 
⇒ ∀p ∈ {1, 2, ..., n}, A[p] ≠ v 
⇒ v ∉ A 

Votre candidat P est utile à cet effet, et les autres ne le sont pas. De plus, vous ne pouvez pas choisir un invariant de boucle - vous devez le prouver afin de prouver que votre algorithme est correct. La nature itérative des boucles se prête à la démonstration par induction, et les invariants comme votre candidat P sont faciles à prouver de cette façon.