Projet : Écrire et prouver des algorithmes itératifs et récursifs
Écrire des algorithmes (simples) en pseudo-code pour résoudre des problèmes algorithmiques.
Maximum d'un tableau
Donnez et prouvez un algorithme récursif de signature :
maximum_rec(t: [réel], n: entier) → entier
Qui rend un indice $0 \leq j \leq n$ tel que $t[j] = \max({t[k] \vert 0\leq k \leq n})$.
corrigé
corrigé
algorithme maximum_rec(t: [réel], n: entier) → entier:
si n == 0:
rendre 0
sinon:
x ← maximum_rec(t, n-1)
si t[x] > t[n]:
rendre x
sinon:
rendre n
Le paramètre n
est un entier qui diminue strictement. Il sera donc à un moment égal à 0 ce qui stoppera la récursion.
La correction se fait par récurrence sur n
allant de n = 0
à n = t.longueur - 1
.
- initialisation : pour
n = 0
, le résultat est clair. - hypothèse de récurrence : on suppose que l'algorithme fonctionne pour
n - 1
- preuve pour
n - 1
. Si l'algorithme fonctionne pourn - 1
,x
contient l'indice max des indices allant de 0 àn - 1
et on rendx
sit[x] > t[n]
etn
sinon : on rend bien l'indice de la valeur maximale du tableau.
Concaténation
Donnez et prouvez un algorithme itératif de signature :
concaténation(début: [entier], fin: [entier]) → [entier]
Qui rend un nouveau tableau contenant la concaténation de début
et de fin
.
corrigé
corrigé
algorithme concaténation(début: [entier], fin: [entier]) → [entier]
t ← tableau de taille début.longueur + fin.longueur
i ← -1
pour chaque j de [0, début.longueur[:
i ← i + 1
t[i] ← début[j]
pour chaque j de [0, fin.longueur[:
i ← i + 1
t[i] ← fin[j]
rendre t
La finitude est claire puisqu'il n'y a que deux boucles de type pour chaque
.
On a deux boucles, il faut donc à priori 2 invariants, un pour chaque boucle. Ici il est clair que l'on va remplir tous les éléments des tableaux début
et fin
dans t
. L'invariant peut être :
si $i_0$ est la valeur de $i$ à la ligne 4 (resp. 8) alors à chaque fin d'itération on a $t[i_0 + 1 + k] == \mbox{début}[k]$ (resp.
fin
) pour tout $0\leq k \leq j$.
Démontrons l'invariant rigoureusement pour la première boucle.
À la fin de la première itération, on a bien :
- $t[i_0 + 1] == \mbox{début}[0]$
- $j = 0$
- $i = i_0 + 1 + j$
Supposons la propriété vraie après une itération donnée. Après une itération supplémentaire, les variables $i$ et $j$ ont été modifiées telles que :
- $j' = j + 1$
- $i' = i + 1 = i_0 + 1 + j'$
L'hypothèse de l'invariant de boucle stipule que $t[i_0 + k] == \mbox{début}[k]$ pour tout $0\leq k \leq j = j'-1$ et comme la boucle a effectué l'affectation : t[i'] ← début[j']
, l'invariant continue d'être vérifié. Ce qui conclut la preuve.
Il faut juste faire très attention à l'endroit on commence dans t
. ici c'est Ok car avant la première boucle i = -1
et i = début.longueur - 1
au début de la seconde boucle. Les éléments de début
et fin
ne vont pas se chevaucher dans t
et se suivre sans interruption.
La preuve de l'invariant dans le corrigé est formelle mais évidente. Il n'est pas nécessaire (et on ne le fera plus) d'être aussi rigoureux pour des boucles aussi simple :
Lorsque le résultat d'une boucle est évidente, il n'est n'est pas nécessaire de faire une preuve formelle (qui sera souvent lourde et inintéressante).
Dans ces cas, contentez vous de donner l'invariant ou le résultat de la boucle.
Suppression de valeurs
Trouver un invariant permet de prouver efficacement un algorithme itératif. Pour des algorithmes simples, les bons invariants sont évidents à prouver une fois trouvé (on ne le donc fera pas explicitement) et permettent une preuve aisée. Entraînez vous avec l'exercice suivant :
Donnez et prouvez un algorithme itératif de signature :
supprime(t: [entier], v: entier) → [entier]
Qui rend un nouveau tableau contenant la restriction de t
aux valeurs différentes de v
.
corrigé
corrigé
Pour que l'algorithme fonctionne, il faut commencer par connaître la taille du tableau à créer et donc compter le nombre d’occurrences de v
dans t
. Ensuite, il sera possible de remplir le tableau.
algorithme supprime(t: [entier], v: entier) → [entier]
nombre ← 0
pour chaque e de t:
si e == v:
nombre ← nombre + 1
t2 ← tableau de taille t.longueur - nombre
j ← 0
pour tout i de [0, t.longueur[:
si t[i] ≠ v:
t2[j] ← t[i]
j ← j + 1
rendre t2
La finitude du programme est clair puisque l'on a que des boucles de type pour chaque
.
On commence à avoir l'habitude des invariants, on peut donc se permettre d'uniquement écrire le résultat d'une boucle si celle ci est évidente. C'est le cas de la première boucle : à l'issue de la boucle des lignes 3-5 nombre
vaut le nombre d'occurrences de v
dans t
.
Pour prouver la seconde boucle, l'invariant peut-être :
à la fin de chaque itération,
t2
contient la restriction desi + 1
premiers éléments det
différents dev
.
La preuve de l'invariant est évidente et permet de prouver l'algorithme en se plaçant à la fin de la dernière itération.
Utilisez l'algorithme concaténation
de la question précédente pour résoudre l'exercice suivant :
Donnez et prouvez un algorithme récursif de signature :
supprime_rec(t: [entier], v: entier) → [entier]
Qui rend un nouveau tableau contenant la restriction de t
aux valeurs différentes de v
. Le nouveau tableau aura la même taille que le tableau t
passé en premier paramètre.
corrigé
corrigé
algorithme supprime_rec(t: [entier], v: entier) → [entier]
si t.longueur == 0:
rendre t
t2 ← tableau de longueur t.longueur - 1
pour i de [0, t2.longueur[:
t2[i] ← t[i + 1]
si t[0] == v:
rendre concaténation([], supprime_rec(t2, v))
sinon:
rendre concaténation([t[0]], supprime_rec(t2, v))
Il n'y a qu'une seule récursion par algorithme et la taille du tableau passé en paramètre est strictement plus petite : il y a un nombre finie de récursion puisque la condition terminale est basée sur une taille nulle de tableau.
Pour la correction une récurrence immédiate sur la taille du tableau nous permet de conclure.
Retournement d'un tableau
Donnez et prouvez un algorithme récursif de signature :
reverse_indice(t: [entier], i: entier) → ∅
Qui modifie le tableau passé en entrée (il ne rend rien !) de telle sorte que les éléments $t[j]$ et $t[t.\mbox{longueur} - 1 - j]$ soit échangés pour tous $i \leq j < t.\mbox{longueur} - i$
corrigé
corrigé
algorithme reverse_indice(t: [entier], i: entier) → ∅
si t.longueur - 1 - i > i:
temp ← t[i]
t[i] ← t[t.longueur - 1 - i]
t[t.longueur - 1 - i] ← temp
reverse_indice(t, i + 1)
Les lignes 3-5 permettent d'échanger les valeurs t[i]
et t[t.longueur - 1 - i]
du tableau. On peut aussi écrire t[i], t[t.longueur - 1 - i] ← t[t.longueur - 1 - i], t[i]
, comme on le ferait en python, si l'on autorise le fait d'affecter 2 valeurs en même temps.
Le finitude est claire puisque :
- il n'y a qu'un appel récursif
- chaque appel se rapproche strictement de la condition d'arrêt
La correction vient du fait que l'on échange bien des valeurs symétriques du tableau par rapport à l'indice du milieu du tableau qui est ici la partie entière de $t.\mbox{longueur} - 1/ 2$.
Lorsque l'on manipule des indices de tableau il faut toujours :
- attentivement vérifier que tout se passe bien.
- faire attention aux divisions entières.
Lorsque l'on crée des algorithmes récursif, on a souvent besoin d'initialiser les paramètres. Par exemple si l'on veut retourner complètement un tableau il faudrait écrire reverse_indice(t: [entier], 0)
. Le paramètre $i$ est un paramètre important pour la récursion mais inutile pour l'appel global. Pour éviter d'avoir des paramètres inutile on encapsulera la fonction récursive dans un algorithme dont le seul but est d'initialiser la récursion. Pour le retournement d'un tableau, l'algorithme sera :
fonction reverse_indice(t: [entier], i: entier) → ∅
... # code de la fonction récursive
algorithme reverse(t: [entier]) → ∅
reverse_indice(t, 0)
La méthode ci-dessus est indispensable à connaître car lorsque l'on manipule des algorithmes récursifs les paramètres font office de variables que l'opn pourrait avoir pour des algorithmes itératifs.
Entraînons nous :
Encapsulez la fonction récursive maximum_rec(t: [réel], i: entier) → entier
du premier exercice dans une fonction permettant de rendre le maximum d'un tableau passé en paramètre.
corrigé
corrigé
algorithme maximum(t: [entier]) → entier
rendre maximum_rec(t, 0)
Récursion terminale
algorithme f(n: A) → B:
si c(n) == Vrai:
rendre g(n)
sinon:
rendre f(h(n))
Où c: A → Booléen
, g: A → B
et h: A → A
sont trois fonctions parfaitement définies.
Pour que la définition de f
ait du sens il faut bien sur que chaque récursion sr rapproche de la condition d'arrêt. C'est ce qu'il faut démontrer pour chaque algorithme sous la forme d'une récursion terminale.
La récursion terminale est sympathique car équivalente à la forme itérative suivante :
algorithme f(n: A) → B:
tant que c(n) est Faux:
n ← h(n)
rendre g(n)
Ce qui permet une implémentation en machine efficace (c'est ce que font les compilateur lorsque'ils repèrent une telle forme).
Le type A
peut être de toute forme, c'est souvent un type composé comme on le verra.
Puissance de deux
Écrivez sous la forme d'une récursion terminale l'algorithme de signature :
algorithme puissance_2(m: entier, n: entier) → entier
Qui rend le plus petit entier de la forme $2^p \cdot m$ plus grand que $n$.
corrigé
corrigé
algorithme puissance_2(m: entier, n: entier) → entier:
si m ≥ n:
rendre m
sinon:
rendre f(2 * m, n)
C'est bien une récursion terminale puisque le code est équivalent à :
fonction c(m: entier, n: entier) → entier:
rendre m ≥ n
fonction g(m: entier, n: entier) → entier:
rendre m
algorithme puissance_2(m: entier, n: entier) → entier:
si c(m, n) == Vrai:
rendre g(m, n)
sinon:
rendre f(2 * m, n)
Avec le type A
étant un couple d'entier et B
le type entier.
Transformer en une forme terminale
La récursion terminale ne fait aucun calcul en propre, il envoie de nouveaux paramètres. Cela semble très restrictif. Par exemple notre fonction factorielle récursive n'est pas sous forme terminale puisque l'on fait un calcul en plus de la récursion :
algorithme factorielle(n: entier # n > 1
) → entier:
si n == 1:
rendre 1
rendre n * factorielle(n-1)
Le rendre récursif terminal est impossible en ne gardant qu'un seul paramètre. L'astuce est d'ajouter un paramètre, appelé accumulateur qui va transmettre à la fonction récursive les calculs intermédiaire, dans notre cas le début du calcul de factoriel. Dans notre cas :
function factorielle_term(n: entier, acc: entier) → entier:
si n == 1:
rendre acc
rendre factorielle(n-1, n * acc)
algorithme factorielle(n: entier # n > 1
) → entier:
rendre factorielle_term(n, 1)
Montrer que l'algorithme précédent :
- est bien sous la forme terminale
- calcule bien la factorielle
corrigé
corrigé
Il est clairement sous la forme récursive terminale. Il fini car chaque récursion se rapproche strictement de la condition d'arrêt.
Enfin, acc
va contenir la factorielle comme le prouve une récursion triviale sur $n$.
La récursion terminale est un moyen efficace d'implémenter des suites arithmétiques ou géométriques. Montrez le :
Donner un prouvez un algorithme écrit sous la forme d'une récursion terminale permettant de calculer tout élément $u_n$ d'une suite arithmétique définie telle que :
corrigé
corrigé
function u_n_term(n: entier,
u0: entier,
r: entier,
acc: entier) → entier:
si n == 0:
rendre u0 + acc
rendre u_n_term(n-1, u0, r, r + acc)
algorithme u_n(n : entier,
u0: entier,
r : entier
) → entier:
rendre u_n_term(n, u0, r, 0)
Transformez l'algorithme récursif précédent en un algorithme itératif.
corrigé
corrigé
Le but de la récursion terminale est de facile,ent transformer un algorithme récursif en un algorithme itératif cr la récursion est une boucle tant que
.
algorithme u_n(n : entier,
u0: entier,
r : entier
) → entier:
acc ← 0
tant que n > 0:
acc ← r + acc
n ← n - 1
rendre u0 + acc
Dichotomie
Le principe de la recherche dichotomique permet de savoir si un entier donné est dans un tableau d'entier trié.
On cherche à savoir si l'entier $v$ est entre les indices $a$ et $b \geq a$ d'un tableau d'entiers $t$. On procède récursivement selon la valeur de $t[\lfloor (a + b)/2 \rfloor]$ :
- si $t[\lfloor (a + b)/2 \rfloor] == v$ on a trouvé l'élément
- si $t[\lfloor (a + b)/2 \rfloor] > v$ on recommence la procédure avec $a' = \lfloor (a + b)/2 \rfloor + 1$ et $b' =b$
- si $t[\lfloor (a + b)/2 \rfloor] < v$ on recommence la procédure avec $a' = a$ et $b' = \lfloor (a + b)/2 \rfloor - 1$
Implémentez cet algorithme de façon récursive avec la signature :
dichotomie_rec(t: [entier],
v: entier,
a: entier,
b: entier # b > a
) → entier: #rend -1 si v n'est pas dans t, l'indice où il est présent sinon
corrigé
corrigé
algorithme dichotomie_rec(t: [entier], v: entier, a: entier, b: entier) → entier:
si b > a:
rendre -1
m ← (a + b) // 2 # division entière
si (t[m] == v):
rendre m
si (t[m] < v):
rendre dichotomie_rec(t, v, m + 1, b)
si (t[m] > v):
rendre dichotomie_rec(t, v, a, m - 1)
Pour la preuve, il suffit de montrer que l'intervalle entre $a$ et $b$ se réduit strictement.
Lorsque l'on code la recherche dichotomique, il faut faire très attention à ce que l'on prend comme milieu et comme condition d'arrêt. Sans quoi votre algorithme risque de tourner indéfiniment.
A priori l'algorithme précédent n'est pas terminal. Le faire :
Utilisez l'algorithme précédent pour écrire l'algorithme qui recherche un élément dans une liste triée de signature :
recherche(t: [entier], v: entier) → entier
corrigé
corrigé
algorithme recherche(t: [entier], v: entier) → entier:
rendre dichotomie_rec(t, v, 0, t.longueur -1)
Fibonacci
La suite de Fibonacci, bien connue, se définie ainsi pour tout $n>0$ :
Utilisez la définition précédente pour créer un algorithme récursif calculant $F_n$ de signature :
fibonacci_rec(n: entier) → entier
corrigé
corrigé
algorithme fibonacci_rec(n: entier) → entier:
si n ≤ 2:
rendre 1
rendre fibonacci_rec(n-1) + fibonacci_rec(n-2)
Il faut démontrer que ce programme est bien un algorithme car il y a plusieurs récursions !
Ceci se fait facilement par une récurrence sur $n$ car chaque appel se rapproche strictement de la condition d'arrêt.
- initialisation : $\mbox{fibonacci\_rec}(n)$ admet un nombre fini de récursion pour $n\leq 2$.
- hypothèse de récurrence : $\mbox{fibonacci\_rec}(m)$ admet un nombre fini de récursion pour $m\leq n$.
- Pour $n + 1$, $\mbox{fibonacci\_rec}(n)$ et $\mbox{fibonacci\_rec}(n-1)$ se terminent en un nombre fini de récursion donc la ligne 4 de l'algorithme aura aussi un nombre fini de récursion.
Une fois la finitude démontrée la correction est évidente, comme souvent avec les algorithmes récursif, puisque l'algorithme ne fait que transcrire l'équation de récursion.
La preuve de l'exercice précédent donne une règle générale de preuve de finitude d'un programme récursif :
À retenir
Si tous les appels récursifs d'un programme se rapprochent strictement de la condition d'arrêt, alors le nombre de récursion est fini.
La condition de rapprochement va dépendre des paramètres et du programme et doit être explicitée.
L'algorithme précédent n'est pas sous la forme de récursion terminale. On peut le rentre terminal en utilisant 2 accumulateurs :
Modifiez l'algorithme récursif précédent pour qu'il devienne une récursion terminale grace à l'utilisation de deux accumulateurs. Cet algorithme sera de signature :
fibo(n: entier, u_i, u_i_moins_un) → entier
Quels seraient les paramètres pour calculer $F_n$ ?
corrigé
corrigé
algorithme fibo(n: entier, u_i, u_i_moins_un) → entier:
si n == 1:
rendre u_i
sinon:
rendre fibo(n-1, u_i + u_i_moins_un, u_i)
Pour calculer $F_n$ :
fibo(n: entier, 1, 0)
Maintenant que la récursion est terminale il est facile de transformer notre algorithme récursif en un algorithme itératif :
Modifiez l'algorithme récursif précédent pour qu'il devienne itératif. Sa signature doit être :
fibo(n: entier) → entier
corrigé
corrigé
algorithme fibo(n: entier) → entier:
u_i ← 1
u_i_moins_un ← 0
tant que n > 1:
temp ← u_i
u_i ← u_i + u_i_moins_un
u_i_moins_un ← u_i
rendre u_i
N'oubliez pas le stockage temporaire de u_i
dans la variable temp
.
Fonction 91 de McCarty
John McCarty fût un informaticien de renom et le créateur du langage Lisp en 1958. Lisp est le premier langage fonctionnel et a été le deuxième langage de programmation au monde, deux ans après le Fortran.
La fonction 91 de McCarty est définie telle que :
Implémentez l'algorithme récursif qui mime la définition.
corrigé
corrigé
algorithme M(n: entier) → entier:
si n > 100:
rendre n - 10
sinon:
x ← M(n + 11)
rendre M(x)
Mais est-ce que ce programme se termine ? Rien n'est moins sur.
Le programme de la question précédente n'est pas forcément un algorithme puisqu'on ne sait pas si les récursion vont s'arrêter. Avant de répondre à cette question, montrons que l'on peut transformer cet algorithme en un programme itératif en appliquant les techniques de la récursion terminale :
Montrez que $M^k(n) = g(n, k)$ avec :
En déduire une version itérative pour résoudre McCarty.
corrigé
corrigé
algorithme M(n: entier) → entier:
c ← 1
tant que c ≠ 0:
si n > 100:
n ← n - 10
c ← c - 1
sinon:
n ← n + 11
c ← c + 1
rendre n
On est pas vraiment sur que cette fonction soit bien définie et donc que le programme ci-dessus soit un algorithme ! Montrons le.
Démontrez que pour tout entier $n$ tel que $90 \leq n < 101$, on a $M(n) = M(n+1)$ et que l'on arrive à cette égalité en un nombre fini de récursion.
corrigé
corrigé
Pour $90 \leq n < 101$, on a :
On arrive à ce résultat en 1 récursion : la ligne 5 de l'algorithme en pseudocode de la question précédente.
Déduire de l'exercice précédent que pour tout $n < 101$, il existe $k\geq 1$ et $90 \leq n < 101$ tel que $M(n) = M^k(n')$.
corrigé
corrigé
Donnez la valeur de $M(n)$ pour tout $n< 101$ et en déduire que la fonction de McCarty est bien définie pour tout entier positif (ie le calcul se fait en un no,bre fini de récursion).
corrigé
corrigé
On a $M(91) = M(91 + 1 + \dots + 1) = M(101) = 91$ et pour tout $n < 90$ on il existera $k > 1$ tel que $M(n) = M^k(91) = 91$
Comme il faut un nombre fini d'itération pour passer de $M(n)$ à $M(n+1)$ on en déduit qu'il faut bien un nombre fini d'itération pour calculer $M(91)$ (disons $I$), et donc également pour calculer $M^k(91)$ quelque soit $k>0$ (il en faut $k\cdot I$).
En donner un algorithme itératif simple pour la calculer.
corrigé
corrigé
algorithme M(n: entier) → entier:
si n > 100:
rendre n - 10
sinon:
rendre 91
Dans le même ordre d'idée que la fonction de Takeuchi.
Récursion croisée
Une dernière technique qui peut être utile est la récursion croisée qui définie une fonction par rapport à une autre et réciproquement :
Écrire les deux fonctions récursives suivantes sans utiliser de division entière :
algorithme pair(n: entier) → booléen
algorithme impair(n: entier) → booléen
Vous pourrez utiliser le fait que pair(0)
est Vrai
alors que'impair(0)
est Faux
.
corrigé
corrigé
algorithme pair(n: entier) → booléen
si n == 0:
rendre Vrai
rendre non impair(n - 1)
algorithme impair(n: entier) → booléen
si n == 0:
rendre Faux
rendre non pair(n - 1)
La finitude est claire puisque :
- il n'y a qu'un appel récursif
- chaque appel se rapproche strictement de la condition d'arrêt
La correction est évidente par définition de la parité.
Triangle de Pascal
Formule du coefficient binomial dit du triangle de Pascal, avec $1\leq k \leq n$ :
et :
Après avoir examiné les conditions d'arrêt, donner un algorithme récursif permettant de calculer le coefficient binomial.
corrigé
corrigé
La formule de récursion s'arrête dans deux cas possibles soit $k = 1$ (première récursion) soit $n - 1 = k$ deuxième récursion. On a alors deux conditions d'arrêts à regarder pour $1\leq k \leq n$ :
- soit $k = 0$ et $\binom{n}{0} = 1$
- soit $k = n$ et $\binom{n}{n} = 1$
On a alors le code :
algorithme binom_rec(n: entier, k: entier) → entier:
si (n == k) ou (k == 0):
rendre 1
sinon:
rendre binom_rec(n-1, k-1) + binom_rec(n - 1, k)
Comme $n$ diminue strictement et $1\leq k \leq n$ on se rapproche strictement de la condition d'arrêt, le programme s'arrête à chaque fois : c'est un algorithme.
Pas de récursion terminale garantie si double récursion. Mais on peut tout de même ici en donner une version itérative. Avant de résoudre l'exercice suivant, regardez comment vous faisiez au lycée en remplissant petit à petit chaque ligne d'une matrice. La ligne $n$ correspond aux coefficients $\binom{n}{k}$ pour tout $0\leq k \leq n$, et vous la remplissiez en utilisant les lignes précédentes avec l'équation. Mais si, rappelez-vous :
Une matrice pourra être construite comme un tableau de (tableaux d'entiers). Si $M$ est est une matrice alors :
- $M$ est de type
[[entier]]
- $M[i]$ est la (i+1) ème ligne de la matrice
- $M[i][j]$ est le (j+1) ème élément de la (i+1) ème ligne de la matrice.
Le code suivant crée une matrice triangulaire inférieure à $n$ lignes valant 1 à toutes les cases du tableau :
algorithme crée_matrice(n: entier) → [[entier]]
matrice ← un tableau de [entier] de taille n
pour chaque i de [1, n]:
ligne ← un tableau d'entiers de taille i
matrice[i-1] ← ligne
pour chaque j allant de 1 à i:
ligne[j-1] ← 1
Utiliser le code précédent pour résoudre l'exercice suivant :
En créant itérativement la matrice triangulaire inférieure, donner une version itérative de l'algorithme calculant le triangle de Pascal. Sa signature devra être :
algorithme binom_matrice(n: entier) → [[entier]]:
corrigé
corrigé
Première version qui calcule toute la matrice triangulaire inférieure :
algorithme binom_matrice(n: entier) → [[entier]]:
matrice ← un tableau de [entier] de taille n+1
pour chaque i de [0, n]:
ligne ← un tableau d'entiers de taille i+1
matrice[i] ← ligne
pour chaque j allant de 0 à i:
si (j == i) ou (j == 0):
ligne[j] ← 1
sinon:
précédent ← matrice[i-2]
ligne[j] ← précédent[j-1] + précédent[j]
rendre matrice
Il y a deux boucles imbriquées, donc deux invariants à trouver !
L'invariant de la boucle 4-13 peut être :
Invariant de la boucle 4-13 :
matrice[i-1]
contient la $i$ème ligne de la matrice triangulaire inférieure de Pascal.
Pour le prouver, il faut trouver un invariant à la boucle 8-13. Par exemple :
Invariant de la boucle 8-13 : si
matrice[i-2]
contient la $i-1$ème ligne de la matrice triangulaire inférieure de Pascal, alorsligne
contient la $i$ème ligne de la matrice triangulaire inférieure de Pascal.
Ce dernier invariant est évidemment vrai par construction de la boucle (c'est la relation de récurrence). Une fois la boucle 8-13 prouvée, cela prouve l'invariant de la boucle 4-13.