/* précondition: l=1 b=1 i=2 */
tant que i<=n
si T[i]>T[i-1] alors
l:=l+1
si l>b alors
b:=l
finsi
sinon l=1
finsi
i:=i+1
ftq
/* postcondition b est la longueur de la plus longue section croissante de
T[1..n] */
i:=1;
tant que i<n faire
si T[i+1] >= T[i]
alors i:=i+1;
sinon
t:=T[i];T[i]:=T[i+1];T[i+1]:=t;
i:=1;
finsi
fintantque;
En utilisant la règle de déduction pour une affectation x:=E;,
à savoir que A(x) est vrai après l'affectation si A(E) était vrai
avant, démontrez formellement que l'assertion ``la partie du tableau de
T[1] à T[i] est triée en ordre croissant'' est vraie après:
p:=liste1 q:=liste2
fu:=nul
tant que p!=nul ou q!=nul
si fu=nul alors
allouer(fu);v:=fu
sinon
allouer(nouveau)
v^.prochain := nouveau
v:= nouveau
finsi
si q=nul ou (p!=nul et p^.valeur<q^.valeur) alors
v^.valeur:=p^.valeur; p:=p^.prochain
sinon
v^.valeur:=q^.valeur; q:=q^.prochain
finsi
ftq
si fu!=nul alors v^.prochain:=nul
/* postcondition : fu pointe vers une nouvelle liste formée des éléments
de liste1 et liste2 en ordre croissant */
debut
x0:=x;
y0:=y;
m:=1;
n:=0;
k:=0;
l:=1;
tant que x!=y faire
si x>y alors
x:=x-y;
m:=m-k;
n:=n-l
sinon
si y>x alors
y:=y-x;
k:=k-m;
l:=l-n
finsi
finsi
fintantque;
retourne x
fin
Modifier la boucle de façon qu'elle calcule les mêmes résultats
par divisions au lieu de soustractions.