i:=1;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:
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;
l'algorithme suivant calcule xn pour n un entier ≥ 0.
xn:=1;
p:=x;
k=n;
tant que k>0 faire
si impair(k) alors
xn:=xn*p;
k:=k-1;
sinon
p:=p*p;
k:=k/2;
finsi;
fintantque;
Donner un invariant qui permettrait de démontrer que la boucle est correcte, c'est-à-dire que ``xn=xn'' est vrai après l'exécution.