Bonjour,

Je suis actuellement en train de réviser les invariants de boucle, terminaison, correcttion ...

J'ai un problème pour l'invariant du tri à bulle, le prof nous a donner ces invariants pour l'algo suivant :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
9
10
11
Pour i=d à f-1 faire
Pour tout x de [d..i-1], T[x]<=T[x+1] et
Pour tout x de [d..i],  pour tout y de [i..f[, T[x]<=T[y] et i<=f



Pour j=f-1 à i Pas -1 faire
Pour tout x de [j+2..f], T[j+1]<=T[x] et j>=i-1



si t[j+1]<t[j] alors échanger(t,j+1,j)
Fin pour
fin pour
Mon problème vient de l'invariant de la deuxieme boucle, en effet l "j+2" pourrai provoquer un débordement puisque j prends au maximum f-1 soit finalement j = f-1 +2 = f+2, donc débordement ?

Cette invariant est il correct, ai-je mal compris ?

Merci de m'expliquer.