Licence Info
Algorithmique Avancée
TD 9 : novembre/décembre 2005
Invariants de boucles

  1. On considère l'algorithme ``TriLent'' qui trie (en ordre croissant) un tableau T, indicé de 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:

    1. après i:=i+1; si elle était vraie avant et aussi T[i+1] >= T[i],
    2. après t:=T[i];T[i]:=T[i+1];T[i+1]:=t; i:=1; si elle était vraie avant, sans autres conditions
  2. Démontrez que ``T est une permutation de T0'' est un invariant de la boucle.
  3. Calcul rapide d'une puissance:

    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.

  4. Donner un invariant de la boucle suivante qui calcule le pgcd de x et y et, en même temps les valeurs m,n telles que ce pgcd est égal à mx+ny.
    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.




File translated from TEX by TTH, version 3.05.
On 6 Dec 2005, 17:33.

symboles bricolés pour netscape par sed