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],
      Réponse La condition citée équivaut à ``Pour tout j < i, T[j]<=T[j+1]''; donc avant l'affectation on a cela et aussi T[i+1] >= T[i], et on peut déduire ``Pour tout j < i+1, T[j]<=T[j+1]'';
      mais cette dernière est exactement équivalente au résultat de la substitution de la partie droite de l'affectation (i+1) pour la partie gauche (i) dans la condition souhaitée.
    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
      Réponse Avant i:=1;, l'assertion ``la partie du tableau de T[1] à T[1] est triée en ordre croissant'' est vraie (parce qu'elle est toujours vraie);
  2. Démontrez que ``T est une permutation de T0'' est un invariant de la boucle.
    Réponse Il faut démontrer que la condition est vraie à la fin d'une itération si elle était vraie avant; et ceci si c'est la partie alors ou la partie sinon qui est exécutée.
    pour la partie alors, c'est simple parce qu'il n'y a pas d'occurrence de i+1 dans la condition;
    pour la partie sinon, on va démontrer que, après les 3 affectations
    t:=T[i];T[i]:=T[i+1];T[i+1]:=t;, on a que ``l'ensemble {T[j] | 1 < =j < i  ou  i+1 < j < =n} U {T[i]} U {T[i+1]} est une permutation de T0'', d'où on déduit trivialement que la condition souhaitée soit vraie.
    On trace la condition qu'il faut prouver de droite à gauche:
    ``l'ensemble {T[j] | 1 < =j < i  ou  i+1 < j < =n} U {T[i]} U {t} est une permutation de T0'' avant T[i+1]:=t,
    ``l'ensemble {T[j] | 1 < =j < i  ou  i+1 < j < =n} U {T[i+1]} U {t} est une permutation de T0'' avant T[i]:=T[i+1],
    ``l'ensemble {T[j] | 1 < =j < i  ou  i+1 < j < =n} U {T[i+1]} U {T[i]} est une permutation de T0'' avant t:=T[i];
    et cette dernière condition est une conséquence directe du supposé invariant avant l'exécution.
  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.

Réponse xn*pk=xn ET k > =0.




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

symboles bricolés pour netscape par sed