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

**Titom78** · 03/08/2011, 15h22

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 :

Sélectionner tout - Visualiser dans une fenêtre à part

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

**Al_th** · 03/08/2011, 17h21

Pseudo-code

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

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 ?

**Franck Dernoncourt** · 03/08/2011, 17h42

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

**Al_th** · 03/08/2011, 19h34

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 :

Sélectionner tout - Visualiser dans une fenêtre à part

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

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

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

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 :

Sélectionner tout - Visualiser dans une fenêtre à part

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

**Franck Dernoncourt** · 03/08/2011, 19h52

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 :

Sélectionner tout - Visualiser dans une fenêtre à part

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)

**pseudocode** · 04/08/2011, 11h25

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

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:

$k = Argmax_{t<=i} (t \; | \; A[t]=v)$