Invariant de boucles — Les-mathematiques.net The most powerful custom community solution in the world

Invariant de boucles

Bonsoir à tous.
Ayant des problèmes de rédaction en informatique, je suis en train de m'exercer, j'aimerais donc que vous regardiez mes différentes rédactions suivantes.

1- Algo.
Fonction Somme(T):
  n=longueur(T)
  s=0
  pour j allant de 1 à n faire
     s=s+T[j]
  finpour
retourner s  
Invariant de boucle.
Soit $j$ un entier non nul
Considérons la proposition P définie par :
$P(j):$ "Après la $j$-ème itération, $s$ contient la somme des éléments $T[1],...,T[j]$".
Preuve.
a- Après la première itération, $s$ contient $T[1]$ donc $P(1)$ est vraie.
b- Supposons que $P(j-1)$ est vraie pour un certain entier $j \geq 2$
Montrons que $P(j)$ est vraie.
Avant la $j$-itération, $s$ contient la somme des éléments $T[1],\ldots,T[j-1]$ càd $s=T[1]+\cdots+T[j-1]$.
Après la $j$-itération , $s=s+T[j]$ càd $s=T[1]+\cdots+T[j-1]+T[j]$.
Donc $s$ contient la somme des éléments $T[1],\ldots,T[j]$, Ainsi $P(j)$ est vraie.
c- En particulier, pour $j=n$, après la $n-$ème itération, $s=T[1]+\cdots+T[n]$, donc l'algorithme renvoie la somme des éléments du tableau.
Conclusion : L'algorithme est correct.

2- Algo.
Fonction Maximum(T):
n=longueur(T)
c=T[1]
pour j allant de 2 à n faire
     si (c<T[j]) alors 
     c=T[j]
  finsi
finpour 
retourner c
Invariant de boucle.
Soit $j$ un entier où $j>1$
Soit la proposition $P$ définie par :
$P(j):$ "Après la $j$-itération, $c$ contient le maximum des éléments $T[1],\ldots,T[j]$".
a- Initialisation.
Pour $j=2$ :
si $T[2]>c$ alors $c=T[2]$ sinon $c=T[1]$, donc dans tous les cas, $c$ contient le maximum des éléments $T[1]$ et $T[2]$.
Donc $P(2)$ est vraie.
b- Supposons que $P(j-1)$ est vraie pour un $j>3$, montrons que $P(j)$ est vraie.
Avant la $j-$itération, $c$ contient le maximum des éléments $T[1],\ldots,T[j-1]$
Si $c<T[j]$ alors $c=T[j]$ sinon $c$ garde sa valeur précédente.
Dans tous les cas $c$ contient le maximum des éléments $T[1],\ldots,T[j]$, ainsi $P(j)$ est vraie.
c- En particulier, pour $j=n$, on a :
après la $n-$ itération, $c$ contient le maximum des éléments $T[1],\ldots,T[n]$.
Donc l'algorithme renvoie le maximum des éléments du tableau.
Conclusion : L'algorithme est correct.

NB : je mettrai le dernier tout à l'heure après mon dîner :-D, merci d'avance.111738

Réponses

  • 3-
    Fonction Position(T):
    n=longueur(T)
    c=0
    pour k allant de 1 à n faire 
         si ($T[k]!=0$) alors
             c=k
         finsi 
    finpour 
    
    retourner c
    
    Invariant de boucles.
    Soit $j$ un entier non nul
    Considérons la proposition $P$ définie par :
    $P(k):$ "Après la $k-$itération, $c$ contient le maximum des indices tels que $j\leq k$ et $T[j]\neq 0$, ou 0 si pour tout $ j\leq k ,\ T[j]=0 $".

    Initialisation : pour $k=1$
    si $T[1]\neq 0$ alors $c=1$ sinon $c=0$.
    Ainsi, après la première itération, $c$ contient le maximum des indices tels que $T[j]\neq 0$ (ici $k=j=1$), ou $0$ avec $T[j]=0$.
    Donc $P(1)$ est vraie.
    Hérédité. Supposons que $P(k-1)$ est vraie pour un certain $k>2$.
    Montrons que $P(k)$ est vraie.
    Avant la $k$-itération, $c$ contient le maximum des indices tels que $j\leq k-1$ et $T[j]\neq 0$ ou $0$ si pour tout $ j\leq k-1 ,\ T[j]=0 $.
    Si $T[k]\neq $ , alors $c$ contient le maximum des indices tels que $j\leq k$ et $T[j]\neq 0$ sinon, contient toujours le maximum des indices tels que $j\leq k$ et $T[j]\neq 0$ ou $0$ si pour tout $ j\leq k ,\ T[j]=0 $.
    Donc $P(k)$ est vraie, donc pour tout $k>0$, $P(k)$ est vraie.

    En particulier, pour $k=n$.
    Après la $n-$ème itération $c$ contient le maximum des indices tels que $T[j]\neq 0$, où $j<k+1$ ou $0$ si pour tout $j<k+1,\ T[j]\neq 0$
    Conclusion. Notre algorithme est correct.
  • Rapidement, sachant que je n'ai lu que la première preuve et ne suis pas prof. d'informatique. J'écrirais plutôt l'algorithme ainsi, de sorte qu'il fonctionne même si la liste en entrée est vide ($n = 0$) :
    Fonction Somme(T):
      n <- longueur(T)
      s <- 0
      j <- 1
      Tant que j <= n faire
         s <- s + T[j]
         j <- j + 1
      Fin tant que
    
      retourner s
    
    Note : <- devrait être écrit $\gets$ et <= devrait être $\leqslant$, mais le logiciel du forum ne supporte pas cela dans le bloc de code.

    Je crois que je définirais l'invariant de boucle de cette façon :
    $P$ : « $s$ est la somme des $j-1$ termes $T[1], \dotsc, T[j-1]$. »
    En convenant du fait que la somme de zéro termes est nulle, $P$ est vraie juste avant la boucle. Ceci permet de faire fonctionner la preuve pour une entrée $T$ vide ($n = 0$) et d'éviter d'analyser deux fois le code de la boucle (itération 1 pour ton $P(1)$ et itération quelconque pour le maintien de l'invariant de boucle). En sortie de boucle, on a dans tous les cas $j = n+1$, donc si on a bien montré que $P$ est vraie à cet endroit-là, on a le résultat souhaité (penser à vérifier que $j = n+1$ en sortie de boucle même si le code intérieur à la boucle n'est pas du tout exécuté, i.e. dans le cas où $n = 0$).

    D'autre part, dans un contexte où l'on utilise des égalités mathématiques comme ici, je n'écrirais pas « Après la $j$-itération, $s=s+T[j]$ » car cette égalité équivaut à $T[j] = 0$. Ne pas confondre l'affectation en pseudo-code $s \gets s+T[j]$ avec l'égalité mathématique $s=s+T[j]$.

    Enfin, bien que l'on puisse effectivement utiliser une récurrence ici, je préfère une structure de preuve un peu plus générale et pas plus difficile :
    • Soit $P$ la propriété (...) (« invariant de boucle », comme celui que j'ai proposé ci-dessus).
    • $P$ est vraie juste avant la répétitive (boucle) car (...).
    • Si $P$ est vraie au début d'une itération quelconque, alors elle est vraie à la fin de cette itération (autrement dit, la répétitive maintient l'invariant de boucle).
    • La répétitive converge (évident pour une boucle « de 1 à $n$ », moins évident pour certaines boucles « Tant que » : il faut prouver, dans ces cas-là, que l'algorithme ne peut pas « boucler indéfiniment »).
    • La propriété $P$ est vraie en sortie de boucle d'après ce qui précède, or elle signifie alors (...), d'où le résultat.
    Ce n'est que mon humble avis, bien entendu.
Connectez-vous ou Inscrivez-vous pour répondre.
Success message!