Licence Info Licence Info
Algorithmique Avancée
TD 9 : décembre 2006
Invariants de boucles

  1. Pour la boucle donnée, répondre par oui ou non aux questions suivantes pour chacune des expressions données:

    1. Est-elle une expression booléenne forcément vraie (si la précondition était vraie) à chaque commencement du calcul de la condition de la boucle?

    2. Est-elle une conséquence de la précondition?

    3. Est-elle forcément vraie à la fin d'une itération de la boucle si elle l'était au début (et que la condition de la boucle était vraie)?

    4. Garantit-elle (étant donné que la condition de la boucle est vraie) que l'itération peut être exécutée sans erreur?

    5. Suffit-elle (avec la négation de la condition de la boucle) pour entraîner la postcondition?
    /* calcul de la partie la plus longue strictement croissante d'une suite donnée dans un tableau [1..n] (n > 1) */ 
    /* 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] */

    1. l-b

    2. i < =n

    3. i > =2

    4. b est la longueur de la plus longue partie croissante de T[1..i]

    5. l est la longueur de la plus longue partie croissante de T[1..i-1] et qui finit T[i-1]

    6. i > =1 et la condition précédente
    Donner un invariant pour laquelle toutes les réponses auraient été OUI.

  2. 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

  3. Démontrez que ``T est une permutation de T0'' est un invariant de la boucle (T0 étant l'ensemble initial des valeurs de T).

  4. fusion de deux listes chaînées
    Donnez un invariant:
    /* précondition : chaque liste liste1 et liste2 est triée en ordre croissant */ 
    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 */

  5. 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 5 Dec 2006, 13:51.