Post-condition: $L$ est inchangée sauf en $i$ et en $j$ où on a :
$$L_f[i] = L_d[j], L_f[j] = L_d[i]$$en notant $L_f$ et $L_d$ les valeurs de $L$ à la fin et au début de l'algorithme respectivement.
def echanger(L,i,j) :
t = L[i]
L[i] = L[j]
L[j] = t
Variant de $B1$ : $V_1 = n - j$. $V_1 = n - i - 1 \in \mathbb N$ avant la boucle car $n - i > 0$ d'après la précondition. Si on a $V_1 \in \mathbb N$ à l'entrée de la boucle, $j < n$ donc $j+1 \leq n$ et $V_1' = n-j' \geq 0 \in \mathbb N$ à la fin de l'itération en notant $V_1'$ et $j'$ les valeurs de $V_1$ et de $j$ à la fin de l'itération de boucle. De plus $V_1' = V_1 - 1$ donc $V_1$ décroit strictement.
Variant de $B2$ : $V_2 = n-i$. $V_2 = n \in \mathbb N$ à l'entrée de la boucle. Si on $V_2 \in \mathbb N$ à l'entrée de la boucle, $i < n-1$ donc $i+1 < n$ et $V_2' = n-i' > 0 \in \mathbb N$ à la fin de l'itération en notant $V_2'$ et $i'$ les valeurs de $V_2$ et de $i$ à la fin de l'itération de boucle. De plus $V_2' = V_2 - 1$ donc $V_2$ décroit strictement.
Avant la boucle, $j = i + 1$ :
On suppose que $I1$ est vrai au début d'une itération de boucle et on note $j'$ et $L'$ la valeur de $j$ et de $L$ à la fin de l'itération. On sait que $j' = j+1$. On a alors à la fin de l'itération :
echanger
agit sur $i$ et $j$ donc ne modifie pas les éléments avant $i$ strictement.echanger
conserve le contenu de la liste.echanger
. Par hypothèse les éléments d'indice $ i < x < j$ sont plus grand strictement
que $L[i]$, donc que $L'[j]$, donc que $L'[i]$. De plus $L'[j]$ est plus grand strictement que $L'[i]$ donc les éléments d'indice $i < x < j'$
sont tous plus grand strictement que $L'[i]$.À la sortie de la boucle l'invariant $I1$ est vrai et de plus $j \geq n$. Donc $j = n$ et la post-condition est bien vérifiée.
Avant la boucle, $i = 0$ :
On suppose que $I2$ est vrai au début d'une itération de boucle et on note $i'$ et $L'$ la valeur de $i$ et de $L$ à la fin de l'itération. On sait que $i' = i+1$.
deplacer_minimum
est vérifiée, donc la post-condition est vrai.deplacer_minimum
ne modifie pas les éléments de départ, donc on a les mêmes éléments qu'on départ.deplacer_minimum
laisse tous ces éléments inchangés, donc il reste triés. deplacer_minimum
nous assure que $L'[i] = L'[i'-1]$ est plus petit strictement
que tous les éléments situés après $i'-1$ non inclus. À la fin de la boucle, $I2$ est donc vrai, et $i \geq n-1$. Les éléments de $L$ sont bien les même qu'au départ d'après l'invariant.
La post-condition est donc vrai.
def deplacer_minimum(L,i) :
for j in range(i+1,len(L)) :
if L[i] > L[j] :
echanger(L,i,j)
def tri_selection(L) :
for i in range(len(L)-1) :
deplacer_minimum(L,i)
L = []
tri_selection(L)
assert L == []
L = [12]
tri_selection(L)
assert L == [12]
L = ([23,12])
tri_selection(L)
assert L == [12,23]
L = ([12,23])
tri_selection(L)
assert L == [12,23]
L = ([12,23,45])
tri_selection(L)
assert L == [12,23,45]
L = ([45,23,12])
tri_selection(L)
assert L == [12,23,45]
L = ([12,45,5,32,25])
tri_selection(L)
assert L == [5,12,25,32,45]
Algorithme tri_fusion
:
Si $L$ est vide ou contient un seul élément :
$\hspace{10px}$ Renvoyer $L$
$m \gets \lfloor \frac n 2 \rfloor$
$L_g \gets$ tri_fusion
($L[:m]$)
$L_d \gets$ tri_fusion
($L[m:]$)
Renvoyer fusion
($L_g$,$L_d$)
Par récurrence sur la taille de la liste.
Initialisation : OK pour taille 0 et 1 Hérédité : Soit $L$ une liste de taille $n > 1$. $1 \leq m < n$
tri_fusion
termine et est correcte sur $L_g$ et $L_d$, donc $L_g$ est triée et $L_d$ est triée. De plus $L_g$ et $L_d$ contiennent à eux deux les éléments de $L$.fusion
. Par hypothèse fusion
termine et est correcte sur $L_g$ et $L_d$. Donc la liste $L'$ renvoyée est triée par ordre croissant et contient exactement les éléments de $L_g$ et de $L_d$, c'est à dire de $L$.def fusion(L1,L2) :
i1, i2 = 0, 0
L = []
while i1 < len(L1) and i2 < len(L2) :
if L1[i1] < L2[i2] :
L.append(L1[i1])
i1 += 1
else :
L.append(L2[i2])
i2 += 1
if i1 == len(l1) :
L += L2[i2:]
else :
L += L1[i1:]
return L
def tri_fusion(L) :
if len(L) < 2 :
return L
m = len(L) // 2
return fusion(tri_fusion(L[:m]), tri_fusion(L[m:]))
L = []
L1 = tri_selection(L)
assert L == []
L = [12]
L1 = tri_selection(L)
assert L == [12]
L = ([23,12])
L1 = tri_selection(L)
assert L == [12,23]
L = ([12,23])
L1 = tri_selection(L)
assert L == [12,23]
L = ([12,23,45])
L1 = tri_selection(L)
assert L == [12,23,45]
L = ([45,23,12])
L1 = tri_selection(L)
assert L == [12,23,45]
L = ([12,45,5,32,25])
L1 = tri_selection(L)
assert L == [5,12,25,32,45]
Variant $V = n_1 + n_2 - i_1 - i_2$. Initialement $V \in \mathbb N$. Dans une itération de boucle, $V' = V + 1$ et dans tous les cas $V' \geq 0$ car $i_1 < n_1$ et $i_2 < n_2$.
Invariant $I3$ :
L'initialisation est évidente car $i_1 = i_2 = 0$ et $L$ est vide.
On suppose que $I3$ est vrai au début d'une itération de boucle et on note $i_1'$, $i_2'$ et $L'$ la valeur de $i_1$, $i_2$ et de $L$ à la fin de l'itération. On a alors à la fin de l'itération :
À la fin de $B3$ on sait que $I3$ et vrai et $i_1 \geq n_1$ ou $i_2 \geq n_2$. On suppose sans perte de généralité que $i_1 \geq n_1$. Donc $i_1 = n_1$. Tous les éléments de $L_2[i_2:]$ sont plus grands que les éléments de $L$ et triés par ordres croissant. $L' = L + L_2[i_2:]$ est donc triée par ordre croissant. Comme $i_1 = n_1$, tous les éléments de $L_1$ sont dans $L$, donc dans $L'$ et d'après l'invariant, tous les éléments de $L_2[:i_2]$ sont dans $L$ donc tous les éléments de $L_2$ sont dans $L'$.