Preuve de correction d'une boucle par invariant : correction d'un exercice

Bonjour à toutes et à tous!

Je me tourne vers vous pour la correction d'un exercice dont voici l'énoncé:

"Considérez le problème de la recherche:
Entrée: Une suite n de nombres A={a1,a2,...,an} et une valeur v,
Sortie: Un indice i tel que v=A[i], ou bien la valeur spéciale NIL si v ne figure pas dans A.

Ecrire le pseudo-code pour recherche linéaire, qui parcourt la suite en recherchant v.
En utilisant un invariant de boucle, montrer la validité de l'algorithme.
Vérifier que l'invariant possède les trois propriétés requises."

Voici ce que j'ai rédigé pour la première question:

Code:

---

1 2 3 4 5 6 7

Pour j=1 de longueursuite A[j]=v // Valeur à rechercher i=j Pour i>0 Si A[i]=v alors retourner i Sinon retourner valeur v=NIL A[i+1]=A[i]

---

Si je ne me trompe pas, l'invariant ici est "i=j"...? Il possède ainsi les trois propriétés requises:
1: à l'initialisation, i=j puisque la l'indice de la valeur cherchée correspond à l'indice du tableau
2: i=j avant l'itération suivante
3: A la terminaison: Bon bah là je ne sais pas quoi répondre...

Est-ce que quelqu'un pourrait me corriger?

D'avance merci

Titom

Pseudo-code

Code:

---

1 2 3 4 5 6 7

POUR i de 1 à n SI A[i] == v ALORS retourner i FINSI FINPOUR retourner NIL

---

Il me semble que ce pseudo-code est plus adapté a une recherche linéaire de valeur dans un vecteur/suite

Ps : Attention a bien séparer le "=" qui veut dire "prend la valeur" et le "=" qui veut dire "egale". Je ne sais pas si tes professeurs t'ont donné une manière de faire, mais sépare les bien (par exemple "<-" pour prend la valeur et "=" pour "egale", ou bien "=" pour "prend la valeur" et "==" pour "egale"). Enfin bref, fais attention

Mais je ne sais pas très bien ce qu'est un invariant de boucle, je vais googlé :)
Cependant, j'ai l'impression que dans tu as écris ton pseudo code pour répondre a la question suivante, je me trompe ?

Citation:

---

Envoyé par Al_th

Mais je ne sais pas très bien ce qu'est un invariant de boucle, je vais googlé :)

---

C'est pour faire de la preuve de correction, une explication ici : http://liafa.jussieu.fr/~gastin/DEUG...tml#Invariants

J'ai effectivement trouvé ce lien en fouinant un peu sur le net, mais je ne vois pas très bien comment l'utiliser dans une recherche linéaire dans un vecteur.

De plus, dans la définition rien ne le lie spécialement a la boucle/algo.

Je suis peut être complêtement débile mais prenons la recherche linéaire.

Code:

---

1 2 3 4 5 6 7 8

// Invariant : i == i POUR i de 1 à n SI A[i] == v ALORS retourner i FINSI FINPOUR retourner NIL

---

Citation:

---

Montrer que I est vrai avant d'entrer dans la boucle.

---

i==i avant d'entrer dans la boucle, tout va bien.

Citation:

---

Montrer que si C et I sont vrais, alors après la liste d'instructions, I est encore vrai.

---

i == i et i < n, dans tout les cas, donc cette proposition est vraie.

Code:

---

1 2	On en déduit que (I et non C) est vrai à la sortie de la boucle (si la boucle termine).

---

Donc i = i et i > n est vraie a la sortie de la boucle.

Si je prend n'importe quelle affirmation qui est toujours vraie ( a=a, 1>2, quand il y a de la neige alors il fait froid), que ce soit avant, pendant, ou après la boucle, ca reste vrai !

Il y a sans doute un point que je n'ai pas saisi a propos de l'invariant de boucle :x

Citation:

---

Preuve par invariant de boucle :

Une preuve d’algorithme par invariant de boucle utilise la démarche suivante :
1) Nous prouvons tout d’abord que l’algorithme s’arrête en montrant qu’une condition d’exécution de boucle finit par ne plus être réalisée.
2) Nous exhibons alors un invariant de boucle, c’est-à-dire une propriété P qui, si elle est valide avant l’exécution d’un tour de boucle, est aussi valide après l’exécution du tour de boucle. Nous vérifions alors que les conditions initiales rendent la propriété P vraie en entrée du premier tour de boucle. Nous en concluons que cette propriété est vraie en sortie du dernier tour de boucle. Un bon choix de la propriété P prouvera qu’on a bien produit l’objet recherché.

La difficulté de cette méthode réside dans la détermination de l’invariant de boucle. Quand on le trouve il est en général simple de montrer que c’est bien un invariant de boucle.

---

(Source : PJ)


Exemple :

Code:

---

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32

Recherche dichotomique dans un tableau trié   i <- 1; j <- N // Inv : 1 <= i <= j <= N et t trié et // x dans t si et seulement si x dans t[i..j] tant que i < j faire // 1 <= i < j <= N et t trié et ... m <- (i+j) div 2 // 1 <= i <= m < j <= N et t trié et ... si x > t[m] alors // 1 <= i <= m < j <= N et t trié et // x dans t si et seulement si x dans t[m+1..j] i <- m+1 // Inv sinon // 1 <= i <= m < j <= N et t trié et // x dans t si et seulement si x dans t[i..m] j <- m // Inv finsi // Inv fin tant que // Inv et i >= j // donc : 1 <= i = j <= N et t trié et // x dans t si et seulement si x = t[i] si x = t[i] alors afficher x, " se trouve en position ", i sinon afficher x, " ne se trouve pas dans le tableau" finsi   Terminaison : j-i >= 0 diminue strictement à chaque itération

---

(Source : http://liafa.jussieu.fr/~gastin/DEUG...20dichotomique)

Citation:

---

Envoyé par Al_th

Si je prend n'importe quelle affirmation qui est toujours vraie ( a=a, 1>2, quand il y a de la neige alors il fait froid), que ce soit avant, pendant, ou après la boucle, ca reste vrai !

Il y a sans doute un point que je n'ai pas saisi a propos de l'invariant de boucle :x

---

Ton invariant de boucle doit être une propriété qui est toujours vraie ET qui permet de valider que ton algo fonctionne.

Le but de ton algo c'est d'obtenir en sortie "[I]Un indice i tel que v=A, ou bien la valeur spéciale NIL si v ne figure pas dans A.". Ton invariant de boucle ca doit donc être une propriété toujours vraie qui permette de valider que la sortie sera correcte.

Par exemple, on peut imaginer une variable intermédiaire "k" dans ta boucle "i" qui vérifie une propriété du genre:

http://latex.codecogs.com/gif.latex?...%20A&#91;t]=v)

:roll:

Petit QCM pour voir si vous avez pigé :)
http://img844.imageshack.us/img844/7...riantpoint.png

Le premier à répondre gagnera une invitation pour Google Music ;)

La réponse (B) (puisque x^k = 1 pour k = 0 ) ;)

Well done :ccool:
PM-moi ton adresse e-mail si tu veux une invite