Invariant de boucles

Réponses

• Gon

  October 2020

  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.
• brian

  October 2020

  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.