Exemples et exercices

1.

Considérez la boucle for_1 presentée en 6.3.

• Dessinnez un tableau qui décrit l'état des variables pour les k premières itérations.
• Quel est l'invariant de cette boucle?
• Montrer son adéquation à la spécification S.

2.

On se donne la spécification:

S_fact : calculer dans la variable fact la factorielle $1 \times 2 \times \ldots (n-1) \times n$ d'un nombre n positif et quelconque.

Ecrire trois versions de ce calcul avec chacune des boucles étudiées: for, loop et while. Pour chaque boucle étudier:

• Exhiber un tableau d'état et un invariant pour chaque boucle. Combien de fois est exécuté chaque boucle?
• Pour chaque boucle, montrer la correction (terminaison et adéquation à la spécification).

3.

Considérez les boucle suivantes, censées réaliser le calcule spécifié par S. Que pouvez-vous dire sur leur correction? Lorsque ces boucles terminent, trouver ce qu'elles calculent.

(a)

      i:= 0;
      while i <= n loop
         i := i + 1;
         somme := somme +i;
      end loop;

(b)

      i:= 1;
      while i <= n loop
         i := i + 1;
         somme := somme +i;
      end loop;

(c)

      i:= 0;
      while i <= n loop
         somme := somme + i;
         i := i + 1;
      end loop;

(d)

      i:= 0;
      loop
         i := i + 1;
         exit when i >= n;
         somme := somme + i;
      end loop;

(e)

      i:= 1;
      loop
         somme := somme + i;
         i := i + 1;
         exit when i >= n;
      end loop;