Licence, Algo 1, TD1, Exercice 2, Question 3.
Soit A un tableau de longueur n (ses indices sont dans l'intervale
[1..n])
On a une fonction rechmin telle que si i£ n et
rechmin(A,i,n)=k alors " jÎ[i..n], A[k]£ A[j].
1exSoit l'algorithme
| |
Pour i de 1 `a n faire |
| |
|
k¬rechmin(A,i,n); |
| |
|
Si i¹ k alors 'echanger A[i] et A[k]; |
| |
Fpour
|
On veut montrer que cet algorithme trie le tableau A, c'est àdire
qu'en fin de calcul on a :
P(A,n) ::-0.1ex= " j1,j2Î[1..n], j1£ j2Þ A[j1]£ A[j2]
Pour cela, on posons
Q(A,i) ::-0.1ex= " j1Î[1..i]," j2Î[i..n] A[j1]£ A[j2]
et l'invariant :
I(A,i) ::-0.1ex= P(A,i)Ù Q(A,i)
En décorant notre code avec les assertions, il faut établir :
| |
Pour i de 1 `a n faire |
| |
|
k¬rechmin(A,i,n); |
| |
|
Si i¹ k alors 'echanger A[i] et A[k]; {I(A,i) } |
| |
Fpour {P(A,i) }
|
Montrons que l'invariant est conservétout au long de l'exécution
de la boucle. Appelons a la valeur de la variable i. On raisonne
par induction sur a³ 1.
(1) Si a=1 (ie : au premier passage dans la boucle), il faut
montrer I(A,1), c'est àdire P(A,1)Ù Q(A,1), c'est àdire
(" j1,j2Î[1..1], j1£ j2Þ A[j1]£ A[j2])
Ù
(" jÎ[1..1], A[j]£ A[1])
Ce qui est vrai car A[1]£ A[1]
(2) Supposons que pour i=a on a I(A,i), c'est àdire I(A,a)
et montrons que pour i=a+1 on a toujours I(A,i), c'est àdire
I(A,a+1). On procéde en deux temps : (a) on montre
Q(A,a+1) puis (b) on montre P(A,a+1).
(a) On veut
" j1Î[1..a+1]," j2,Î[a+1..n]A[j1]£ A[j2]
Par hypothèse de récurrence, on a
" j1Î[1..a]," j2,Î[a..n], A[j1]£ A[j2]
Puisque k est le résultat de rechmin(a+1,n), en appelant
b la valeur de A[k] on a que
" j2Î[a+1..n], b£ A[j2]
avec kÎ[a+1..n], aprés exécution de la première
instruction. On raisonne alors par cas suivant le résultat du test
a+1¹ k.
Si a+1¹ k, on a procédéàl'échange donc la valeur
présente en A[a+1] est b.
Sinon, comme k=a+1, on a encore A[a+1]=b.
Dans les deux cas, on a
" j2Î[a+1..n], A[a+1]£ A[j2]
De plus, comme on a, par hypothèse de récurence, en prenant
j2=k
" j1Î[1..a], A[j1]£ b
ce qui nous donne
" j1Î[1..a], A[j1]£ A[a+1]
En recollant ensemble les morceaux, on a bien ce que l'on voulait.
(b) On veut
" j1,j2Î[1..a+1], j1£ j2Þ A[j1]£ A[j2]
Par hypothése de récurence, on a
" j1,j2Î[1..a], j1£ j2Þ A[j1]£ A[j2]
On a montréen (a) que
" j1Î[1..a], A[j1]£ A[a+1]
On a donc bien ce que l'on veut.
En sortie de boucle, i vaut n, l'invariant
nous donne donc, en particulier : P(A,n).
This document was translated from LATEX by HEVEA.