Cette invariance de boucle est-elle correcte?

Question

Le pseudo-code pour la boucle de recherche linéaire:

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

boucle invariante J'ai écrit:

Au début de chaque itération de la boucle, j est le prochain indice après où A [j-1] n'est pas égal à v.

Initialisation:

Lorsque j est égal à 1 et avant de vérifier si elle est moindre que a.length, l'indice précédent est . Alors A [0] n'est pas égal à v, car dans ce contexte A [0] n'existe même pas.

Entretien:

Si A [j] est égal àv puis la boucle se termine. Ce qui signifie que nous n'avons pas l'itération suivante. Mais si elle n'est pas égale à v alors l'itération suivante de la boucle s'exécute tout en préservant l'invariant de boucle.

terminaison:

Les conditions provoquant la boucle pour mettre fin sont que j est plus grande que a.length ou v est égal àA [j]. Parce que chaque itération de boucle augmente j par , nous avons vérifié tous les éléments de A contre v jusqu'à j est plus grande que a.length. D'où l'algorithme est correct. Si v est égal à A [j] alors cela signifie que nous avons trouvé l'élément que nous avons cherché. Ainsi, l'algorithme est correct.

Est-ce correct?

Answer 1

Ce n'est pas si mal, mais vous pourriez apporter quelques améliorations.

Invariant de boucle: Le langage "next after where ..." est maladroit, et vous ne l'utilisez pas dans la preuve que l'algorithme est correct, donc il n'y a pas de raison de le maintenir. Quelque chose comme ceci serait mieux: "Au début de chaque itération, il n'existe aucun i < tel que A [i] == v". La maintenance: La boucle continue si A [j]! = V. Puisqu'il n'existe aucun i < j tel que A [i] == v, et A [j]!= v, alors il n'existe pas non plus de i < = j tel que A [i] == v, et l'invariant de boucle est valable pour la plus grande valeur suivante de j.

Ensuite, vous pouvez l'utiliser dans la condition de terminaison: La boucle se termine tôt si elle trouve v dans le tableau et renvoie son index. Sinon, l'invariant de boucle est valable pour j == longueur + 1, et il est connu qu'il n'existe pas de longueur < = telle que A [i] == v, c'est-à-dire que v ne se produit pas dans le tableau.