Invariant de boucles

Gon · October 2020

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

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.

Invariant de boucles

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 32