Précédent Remonter Suivant
Chapitre 5 Correction

L a programmation est une activité complexe, peut-être même une des plus complexes jamais imaginées par l'homme. En mathématiques standards, les variables sont souvent rangées en vecteurs, tableaux ou tenseurs. En informatique, le nombre de variables manipulées par un programme est souvent très grand, les variables sont plutôt indépendantes en dépit de la structuration des données et du regroupement des intructions en fonctions ou en modules. En outre, un programme s'exécute sur un grand nombre de données (ce nombre peut même être infini). Au total, il est délicat de savoir si un programme est correct. La validation des programmes a fait l'objet de nombreuses études et reste un domaine important de la recherche actuelle. On peut chercher à trouver un jeu de tests représentatifs, mais cette méthode n'est pratiquement jamais exhaustive. On peut aussi démontrer mathématiquement que le résultat d'un programme vérifie certaines propriétés. Malheureusement, les démonstrations sur les programmes sont souvent longues et peu intéressantes, à la grande différence des démonstrations des mathématiques, plutôt courtes et conceptuelles. Néanmoins les preuves de programmes sont importantes pour garantir le bon fonctionnement d'un logiciel. C'est pourquoi on cherche à faire les preuves de correction de programmes rigoureusement, c'est-à-dire en utilisant un langage spécial, celui de la logique mathématique, définie par Hilbert, Frege, Gödel et Herbrand. Il n'est pas question ici d'étudier la logique mathématique, qui fait l'objet de longs développements à elle seule. Nous nous contenterons de décrire la méthode des assertions de Floyd et de Hoare.

Dans ce chapitre, nous considérerons la correction de programmes itératifs simples manipulant des scalaires, puis la validation de programmes itératifs manipulant des tableaux, et celle de programmes récursifs avec le principe d'induction. Il sera aussi question de la terminaison des programmes.

5.1 Correction de programmes itératifs scalaires

La suite de Fibonacci définie par u0 = 0, u1 = 1, un = un-2 + un-1 pour n > 1 est une suite linéaire récurrente d'ordre 2. On peut calculer chacun de ses termes en temps constant, en calculant les racines de l'équation caractéristique associée r2 - r - 1 = 0. Ici nous considérons des calculs moins sophistiqués pour chaque terme un qui prennent un temps en O(n).
int fib (int n) {
  int[ ] tab = new int[n+1];
  tab[0] = 0; tab[1] = 1;
  for (int i = 2; i <= n; ++i)
    tab[i] = tab[i-2] + tab[i-1];
  return t[n];
}

Comme déjà discuté pour la programmation dynamique dans le chapitre 4, le tableau de n+1 entiers est inutile, car seulement les deux dernières valeurs x et y suffisent. On peut se contenter de faire le calcul de fib(n) par la fonction suivante:
static int fibonacci (int n) {
  int x = 0;
  if (n != 0) {
    x = 1; int y = 0;
    for (int k = 1; k != n; ++k) {
      int t = y;
      y = x;
      x = x + t;
    }
  }
  return x;
}

Même si cette optimisation est souvent inutile, car les n-1 cases mémoire gagnées sont dérisoires devant la taille des mémoires des ordinateurs modernes, le programme résultant est intéressant, car il a un degré de complexité supplémentaire. Par complexité nous signifions ici la complexité dans son sens naturel, c'est-à-dire la non-simplicité de la solution. En effet, les variables x et y doivent être initialisées, puis modifiées dans le bon ordre de manière à ce qu'aucune d'entre elles ne soit écrasée avant l'utilisation de sa valeur précédente. Nous nous efforçons de montrer rigoureusement que ce programme est correct.



En commentaires, nous plaçons une assertion logique d'entrée P au début de la fonction et une assertion de fin R sur le résultat final. Pour que le programme soit correct, il s'agit de montrer que si P est vérifiée, il en est de même pour l'assertion Q.
static int fibonacci (int n) {
  // P= {n ³ 0}
  int x = 0;
  if (n != 0) {
    x = 1; int y = 0;
    for (int k = 1; k != n; ++k) {
      int t = y;
      y = x;
      x = x + t;
    }
  }
  // Q= {x = fib(n)}
  return x;
}

Pour cela, nous allons considérer une troisième assertion I, dite assertion de boucle ou encore invariant de boucle, qui sera vraie au début de chaque itération. Pour que l'emplacement de cet invariant dans le programme soit plus clair, l'instruction for est décomposée en une instruction d'affectation pour l'initialisation de la variable de contrôle et une instruction d'itération while. Graphiquement, l'emplacement de ces assertions est aussi représenté sur l'organigramme de la figure 5.1.

Figure 5.1 : Organigramme d'un programme avec ses invariants


static int fibonacci (int n) {
  // P= {n ³ 0}
  int x = 0;
  if (n != 0) {
    x = 1; int y = 0;
    int k = 1;
    // I = {k £ nÙ x = fib(k)Ù y = fib(k-1)}
    while (k != n) {
      int t = y;
      y = x;
      x = x + t;
      ++k;
    }
  }
  // Q= {x = fib(n)}
  return x;
}

Pour simplifier, nous supprimons les symboles de commentaires et laissons les assertions entre accolades, sans qu'il n'y ait d'ambiguité avec celles utilisées en Java:
static int fibonacci (int n) {
  {n ³ 0}
  int x = 0;
  if (n != 0) {
    x = 1; int y = 0;
    int k = 1;
    {k £ nÙ x = fib(k)Ù y = fib(k-1)}
    while (k != n) {
      int t = y;
      y = x;
      x = x + t;
      ++k;
    }
  }
  {x = fib(n)}
  return x;
}

Il ne reste plus à montrer que de P on peut dériver I, que I est invariant à chaque itération, que de I on dérive Q quand on sort de la boucle, et que de P on dérive Q quand on ne passe pas dans la boucle. Pour cela, on introduit des assertions intermédiaires à vérifier après chaque instruction élémentaire, et il suffit de montrer que chacune d'entre elles est vraie dès que l'assertion précédant l'instruction en question est vraie.
1      static int fibonacci (int n) {
2        {n ³ 0}
3        int x = 0;
4        {n ³ 0 Ù x = 0}
5        if (n != 0) {
6          x = 1; int y = 0;
7         {n > 0Ù x = fib(1)Ù y = fib(0)}
8         int k = 1;
9         {0 < k £ nÙ x = fib(k)Ù y = fib(k-1)}
10        while (k != n) {
11          {0 < k < nÙ x = fib(k)Ù y = fib(k-1)}
12          int t = y;
13          {0 < k < nÙ x = fib(k)Ù y = fib(k-1) Ù t = fib(k-1) }
14          y = x;
15          {0 < k < nÙ x = fib(k)Ù y = fib(k) Ù t = fib(k-1) }
16          x = x + t;
17          {0 < k < nÙ x = fib(k+1)Ù y = fib(k) Ù t = fib(k-1) }
18          ++k;
19        }
20        {k = nÙ x = fib(k)Ù y = fib(k-1)}
21      }
22      {x = fib(n)}
23      return x;
24     }

Notons Pn l'assertion de la ligne n et Pm |-f Pn quand de l'assertion Pm on peut dériver Pn dans le code de la fonction f (Ici f=fibonacci). On écrira aussi Pm |- Pn quand f est clair d'après le contexte. Donc, dans le code de la fonction fibonacci, on a trivialement P2 |- P4. De même P4 |- P7, puisqu'alors x = 1 = fib(1) et y = 0 = fib(0). Par ailleurs, n ¹ 0 puisque nous venons de franchir le test de la ligne 5, et n > 0 puisque n ³ 0 à cause de P4. Maintenant P7 |- P9, puisque, sur la ligne 9, on a alors k = 1. Montrons que P9 |- P20 quand on sort de la boucle. Alors le test de la ligne 10 est faux, et donc k = n, et on a P20. On en déduit P22 puisque P20 Þ P22. Il reste à montrer que l'invariant de boucle I = P9 est bien préservé à chaque itération.

D'abord P9 |- P11, puisque le franchissement du test de la ligne 10 indique k ¹ n. De même, on a facilement que P11 |- P13 et P13 |- P15. La preuve que P15 |- P17 est un peu plus complexe. En effet, l'exécution de l'instruction de la ligne 16 ne modifie que la valeur de x . Après cette instruction, on a donc x = fib(k) + fib(k-1), puisqu'avant cette instruction, d'après P15, on a x = fib(k) et t = fib(k-1). Comme 0 < k, on a fib(k+1) = fib(k) + fib(k-1). Donc x = fib(k+1). Montrons finalement que P17 implique l'invariant de boucle P9. Entre les deux, on ne fait qu'incrémenter la valeur de k. Il suffit donc de remplacer k+1 par k dans la formule de P17 pour obtenir P9. Ceci est obtenu facilement puisque x = fib(k+1) devient x = fib(k), et y = fib(k+1 -1) devient y = fib(k-1). De même 0 < k+1 - 1 < n devient 0 < k - 1 < n, c'est-à-dire 0 < k £ n.

On peut considérer l'organigramme de la figure 5.1 (complété avec toutes les assertions intermédiaires) comme un graphe dont les sommets sont les assertions et les arcs les instructions. On considère tous les chemins menant de l'assertion d'entrée à l'assertion de sortie. Le nombre de ces chemins peut être infini. Mais, il s'expriment tous par composition de trois chemins simples (c'est-à-dire qui ne passent pas deux fois par un même sommet intermédiaire): les chemins de l'assertion d'entrée P à l'invariant de boucle I, de I à I et de I à Q. C'est ce shéma que nous avons suivi précédemment pour démontrer que P |- Q.

Considérons un deuxième exemple en posant des assertions sur le calcul du PGCD.
static int pgcd (int a, int b) {
  int x = a, y = b;
  while (x != y)
    if (x > y)
      x = x - y;
    else
      y = y - x;
  return x;
}

Il s'agit de montrer que si a et b sont deux entiers strictement positifs, le résultat final est bien le PGCD. On décore le programme précédent avec toutes les assertions intermédiaires.
1      static int pgcd (int a, int b) {
2        {a > 0 Ù b > 0}
3        int x = a, y = b;
4        {x > 0 Ù y > 0 Ù pgcd(x,y) = pgcd(a,b)}
5        while (x != y) {
6          {x > 0 Ù y > 0 Ù x¹ y Ù pgcd(x,y) = pgcd(a,b)}
7          if (x > y) {
8            {x > 0 Ù y > 0 Ù x > y Ù pgcd(x-y,y) = pgcd(a,b)}
9            x = x - y;
10           {x > 0 Ù y > 0 Ù pgcd(x,y) = pgcd(a,b)}
11         } else {
12           {x > 0 Ù y > 0 Ù x < y Ù pgcd(x,y-x) = pgcd(a,b)}
13           y = y - x;
14           {x > 0 Ù y > 0 Ù pgcd(x,y) = pgcd(a,b)}
15         }
16       }
17       {x > 0 Ù x = y = pgcd(x,y) = pgcd(a,b)}
18       return x;
19     }

A nouveau, Pn désigne l'assertion de la ligne n. Les preuves de P6 |- P8 et de P6 |- P12 reposent sur des propriétés arithmétiques du PGCD. Pour P8 |- P10, on remplace simplement x-y par x. De même pour P12 |- P14, c'est y-x qui est remplacé par y.
Exercice 26   Montrer que le raisonnement n'est plus valide avec {a ³ 0 Ù b ³ 0} comme assertion d'entrée. Comment corriger le programme?

Exercice 27   Montrer que l'algorithme (d'Euclide) suivant calcule aussi le PGCD:
static int pgcd (int a, int b) {
  int x = a, y = b;
  while (y != 0) {
    int r = x % y;
    x = y;
    y = r;
  }
  return x;
}

5.2 Correction de programmes itératifs avec des tableaux


La méthode des assertions marche aussi avec des structures de données composites, comme les tableaux. Nous considérons le programme du drapeau hollandais défini par Dijkstra, qui consiste à faire en place un tri à trois valeurs. Au début, un tableau ne contient que des éléments bleus, blancs et rouges. On veut trier le tableau en regroupant d'abord les éléments bleus, puis les blancs et enfin les rouges. Tout cela doit se faire en une seule passe sans mémoire auxiliaire comme indiqué sur la figure 5.2. Pour tout élément ai, on regarde sa couleur et on le permute avec ab ou ar selon les cas. Ce qui donne le programme suivant:

Figure 5.2 : Le drapeau hollandais

static void drapeauHollandais (int[ ] a) {
  int b = 0, i = 0, r = a.length;
  while (i < r) {
    switch (a[i]) {
    case BLEU:
      int t = a[b]; a[b] = a[i]; a[i] = t;
      ++b; ++i;
      break;
    case BLANC:
      ++i;
      break;
    case ROUGE:
      --r;
      int u = a[r]; a[r] = a[i]; a[i] = u;
      break;
    }
  }
}

L'invariant de boucle spécifie les zones où la couleur reste constamment bleu, blanc ou rouge, grâce au prédicat f défini par
f(i,j,c)  =  0 £ i £ j £ n  Ù  " k .  i £ k < j Þ a[k] = c
Avec ses assertions, le programme est donc comme suit:
static void drapeauHollandais (int[ ] a) {
  int b = 0, i = 0, r = a.length, n = r;
  {f(0,b,BLEU) Ù f(b,i,BLANC) Ù f(r,n,ROUGE)}
  while (i < r) {
    switch (a[i]) {
    case BLEU:
      {f(0,b,BLEU) Ù f(b,i,BLANC) Ù f(r,n,ROUGE) Ù a[i] = BLEU}
      int t = a[b]; a[b] = a[i]; a[i] = t;
      {f(0,b+1,BLEU) Ù f(b+1,i+1,BLANC) Ù f(r,n,ROUGE)}
      ++b; ++i; break;
    case BLANC:
      {f(0,b,BLEU) Ù f(b,i+1,BLANC) Ù f(r,n,ROUGE)}
      ++i; break;
    case ROUGE:
      {f(0,b,BLEU) Ù f(b,i,BLANC) Ù f(r,n,ROUGE) Ù a[i] = ROUGE}
      --r;
      {f(0,b,BLEU) Ù f(b,i,BLANC) Ù f(r+1,n,ROUGE) Ù a[i] = ROUGE}
      int u = a[r]; a[r] = a[i]; a[i] = u;
      break;
  } }
  {f(0,b,BLEU) Ù f(b,r,BLANC) Ù f(r,n,ROUGE)}
}

Manipuler des tableaux ne produit pas de difficultés supplémentaires dans la méthode des assertions. Il faut raisonner sur les valeurs et les indices des tableaux. On peut aussi remarquer que le programme fonctionne aussi pour le tableau vide (n = 0).
Exercice 28   Montrer la correction du programme de tri par sélection.

5.3 Correction partielle et logique de Hoare


On peut tirer un certain nombre de principes généraux des preuves de correction vues sur les exemples précédents. Ces principes seront énoncés de manière intuitive ici, mais ils peuvent être complètement formalisés pour définir les axiomes et les règles d'inférence d'une logique de programmes souvent appelée logique de Hoare.

D'abord, les assertions n'ont de sens que placées par rapport à un programme, puisqu'une assertion peut-être vraie à un endroit du programme, mais fausse à un autre endroit. Les termes de notre logique sont de la forme {P} S {Q}, où P et Q sont deux formules logiques et S un (bout de) programme. Les formules P et Q sont des pré-conditions et post-conditions de l'instruction S.

Une première remarque consiste à énoncer que pour montrer la post-condition P(x) après une instruction d'affection de x par une expression E, il suffit d'avoir P(E) valide comme pré-condition. Donc un premier axiome de notre logique est:
{P (E)}  x = E; {P(x)}
De même, si on veut montrer
{P}  if (E) S else S' {Q}
il faut montrer
{P Ù E}  S {Q}      et      {P Ù ¬ E}  S' {Q}
Enfin, pour montrer
{P}  while (E) S {Q}
il faut deviner l'invariant I, et montrer P Þ I et I Ù ¬ E Þ Q et
{I Ù E}  S {I}
Trouver l'invariant de boucle fait partie de la difficulté des preuves de correction; mais c'est toujours un bon effort pour arriver à la correction du programme ou tout au moins pour le rendre plus robuste.

D'autres règles existent pour les constructions restantes du langage de programmation. Nous remarquons finalement que la règle pour l'instruction while peut être simplifiée, si on ajoute une règle de transitivité. En effet, si P implique P' et si Q' implique Q, alors pour obtenir P et Q comme pré et post-conditions valides de S, il suffit de montrer que P' et Q' sont des pré et post-conditions valides de S. Autrement dit, pour obtenir
{P}  S {Q}
il suffit de montrer
P Þ P'        {P'}  S {Q'}        Q' Þ Q

Traditionnellement les règles de la logique sont présentées avec les prémisses et les conclusions de chaque règle au-dessus et en-dessous d'une ligne horizontale. Pour un axiome, il n'y a aucun prémisse; l'axiome figure en dessous de la ligne horizontale. Pour une règle d'inférence, les hypothèses figurent au-dessus, la conclusion figure en-dessous. Ainsi, la mini-logique de Hoare que nous venons de voir est résumée par 6 règles sur la figure 5.3 avec concision et précision.
              
  
{P (E)}   x = E;   {P(x)}
    
{P Ù E}   S   {Q}      {P Ù ¬ E}   S' {Q}
{P}   if (E) S else S'   {Q}
  
  
{P}   S  {Q}    {Q}   S' {R}
{P}    S S' {R}
    
{P}   S  {Q}
{P}    \{S\}   {Q}
  
  
{P Ù E}   S  {P}
{P}   while (E) S  {P Ù ¬ E}
    
P Þ P'    {P'}   S  {Q'}    Q' Þ Q
{P}   S  {Q}
  

Figure 5.3 : Logique de Floyd-Hoare

La logique de Hoare manipule des assertions dans les programmes. Ces assertions sont censées être vérifiées à chaque fois que le programme passe par leurs emplacements. Mais rien ne garantit que le programme passe à un emplacement donné. Ainsi quand on écrit {P} S {Q}, on sait que si on démarre l'instruction S avec l'assertion P vraie, alors l'assertion Q est vérifiée si on termine S. Mais on n'a aucune garantie sur la terminaison de S. Donc la correction d'un programme par la méthode des assertions, vue jusqu'à présent, dit que l'assertion de fin est vraie si on démarre avec l'assertion de départ également vraie; mais il n'est pas sûr que le programme termine. Par exemple
{true}   while (true) S;  {P}
est vraie pour tout P et tout S, puisque jamais P ne sera atteint. Comme on n'a aucune indication sur la terminaison des programmes, on dit que la correction obtenue est une correction partielle.

Enfin, il faut comprendre que les assertions de correction d'un programme sont distinctes de ses spécifications. Les spécifications, parfois aussi appelées le ``le cahier des charges ``, forment un concept souvent informel. L'adéquation des assertions de correction d'un programme avec ses spécifications n'est pas toujours claire. Il se peut qu'on prouve correcte une assertion ne répondant pas aux spécifications. La correspondance entre spécifications et programmes peut se faire progressivement par couches successives, par rafinements successifs. Les spécifications relèvent parfois de méthodologies quelque peu miraculeuses. Il existe aussi des systèmes formels pour spécifier les programmes. Cela est particulièrement important quand on veut faire du zéro-fautes, dans des programmes critiques, tels que les systèmes embarqués pour les transports ou le guidage de missiles, ou les protocoles de sécurité dans les transactions commerciales, ou encore les programmes de conception des circuits intégrés.

5.4 Implémentation des assertions

Les langages modernes ont tous un système d'assertions. En Java 1.4, il existe une instruction spéciale assert, qui lève une erreur si l'assertion n'est pas vérifiée. On retrouve aussi cette instruction en Caml, C, C++. En Java 1.1.8, il n'y a pas de système d'assertions, mais il est toujours possible d'écrire sa propre classe.
class AssertionError extends Error { }

public class Assertion {
  public static void check (boolean e) {
    if (!e) throw new AssertionError();
  }
}

On peut passer en argument de Assertion.check une expression booléenne quelconque correspondant à l'assertion à tester. Bien sûr, pour les assertions avec des quantificateurs universels ou existentiels sur des espaces infinis, c'est plus délicat (quelquesoit le langage de programmation!).

Ecrire des assertions dans ses programmes est toujours recommandé. Les systèmes d'exécution peuvent les désarmer sans modifier les programmes en mode de fonctionnement opérationnel. Mais le surcoût engendré par leur vérification est souvent faible devant le gain en fiabilité obtenu en gardant les assertions actives.
5.5 Fonctions et récursion

Le découpage des programmes en fonctions n'induit pas de difficultés supplémentaires dans la méthode des assertions. Il suffit d'avoir une assertion d'entrée et de sortie pour chaque fonction. Pour les programmes récursifs, il en va de même. Prenons l'exemple du calcul récursif de factorielle.
static int fact (int n) {
  int r;
  if (n == 0)
    r = 1;
  else
    r =  n * fact(n-1);
  return r;
}

On veut montrer la formule: " k.  k ³ 0 Þ fact(k) = k!. Pour cela, on suppose, comme pour les invariants de boucles, que les appels récursifs utilisés vérifient déjà cette formule, et on montre qu'elle reste invariante dans le corps de la fonction. On a donc les deux assertions suivantes d'entrée et de sortie dans le corps de la fonction:
static int fact (int n) {
  int r;
  {n ³ 0 Ù " k.   k ³ 0 Þ fact(k) = k! }
  if (n == 0)
    r = 1;
  else
    r =  n * fact(n-1);
  {r = n!}
  return r;
}

et en complétant avec les assertions intermédiaires
1       static int fact (int n) {
2         int r;
3        {n ³ 0 Ù " k.   k ³ 0 Þ fact(k) = k!  }
4        if (n == 0) {
5          {n = 0  }
6          r = 1;
7          {n = 0 Ù r = 1 = 0!}
8        } else {
9          {n-1 ³ 0 Ù fact(n-1) = (n-1)! }
10         r =  n * fact(n-1);
11         {r = n (n-1)! = n!  }
12       }
13       {r = n!}
14       return r;
15     }

Remarquons que P3 |- P9 par instanciation. En effet, à la ligne 9, on a P3 Ù n ¹ 0, et donc n > 0. En utilisant la partie quantifiée universellement de P3, on a fact(n-1) = (n-1)! sur la ligne 9, et donc P9 est vrai. Le reste se dérive aisément. A nouveau, il ne s'agit que de correction partielle. Un autre argument doit être utilisé pour démontrer la terminaison. Remarquons aussi qu'on n'a pas fait de récurrence sur les entiers, mais simplement supposé l'invariant de sortie vrai pour l'appel récursif. Ce principe de raisonnement est aussi valide pour plusieurs fonctions s'appelant entre elles.
Exercice 29   Montrer que, pour tout P, on a {true} x=f(n); {P} quand f est définie par: static int f(int n) { return f(n);}.

Un deuxième exemple de correction de programme récursif fait intervenir des listes: c'est le programme élémentaire d'insertion d'un élément dans une liste triée
static Liste inserer (int x, Liste a) {
  int r;
  if (a == null || x < a.val) {
    r = new Liste(x, a);
  } else if (a.val < x) {
    r =  new Liste(a.val, inserer(x, a.suiv));
  } else
    r = a;
  return r;
}


On cherche à montrer " a." x. ord(a) Þ ord(inserer(x,a)) où ord(a) signifie que la liste a est ordonnée, c'est-à-dire que si a est la liste contenant la suite á a1, a2, ... anñ (n ³ 0), on a a1 £ a2 £ ... an. On peut aussi définir récursivement ce prédicat par:
ord(a) = (a ¹ null Ù a.suiv ¹ null  Þ   a.val £ a.suiv.val Ù ord(a.suiv))
Nous avons aussi besoin de l'ensemble des éléments d'une liste a défini par:
ens(a) = ì
í
î
Ø   si  a = null
{  a.val  } È ens(a.suiv)   sinon
Et on montre que l'on a aussi:
" a." x. ens(inserer(a,x)) Ì {x} È ens(a)
Toutes les assertions intermédiaires figurent sur le programme suivant:

1      static Liste inserer (int x, Liste a) {
2        int r;
3        { ord(a)  Ù  " a." x. ord(a) Þ ord(inserer(x,a)) Ù
" a." x. ens(inserer(a,x)) Ì {x} È ens(a) }
4        if (a == null || x < a.val) {
5          {ord(a) Ù (a ¹ null Þ x < a.val) }
6          r = new Liste(x, a);
7          {ord(r) Ù ens(r) = {x} È ens(a) }
8        } else if (a.val < x) {
9          {ord(a) Ù a ¹ null Ù a.val < x Ù ord(inserer(x,a.suiv)) Ù
ens(inserer(x,a.suiv)) Ì {x} È ens(a.suiv) }
10         r =  new Liste(a.val, inserer(x, a.suiv));
11         {ord(r) Ù ens(r) Ì { x } È ens(a)}
12       } else {
13         { ord(a) }
14         r = a;
15         {ord(r) Ù ens(r) = ens(a)}
16       }
17       {ord(r) Ù ens(r) Ì {x} È ens(a)}
18       return r;
19     }

Les raisonnements non triviaux font passer de P5 à P7, et de P9 à P11. Pour le premier cas, on remarque que si a = null, alors r est une liste singleton et donc ord(r). Si a ¹ null, alors x < a.val et donc, comme r est la liste contenant x puis continuant par la liste ordonnée a, on a aussi ord(r). Pour le second cas, si P9 est vrai, on sait, sur la ligne 11, que r est la liste contenant a.val puis continuant par la liste ordonnée inserer(x,a.suiv). Or comme a.val < x et comme ord(a) est vrai, on a a.val < y pour tout y Î {x} È ens(a.suiv). Comme ens(inserer(x,a.suiv)) Ì {x} È ens(a.suiv), on a aussi a.val < y pour tout y Î ens(inserer(x,a.suiv)). D'où ord(r). Par ailleurs, par P9, on a ens(inserer(x,a.suiv)) Ì {x} È ens(a.suiv). D'où on déduit pour le résultat r que ens(r) Ì {a.val} È {x} È ens(a). Comme a ¹ null, on obtient ens(r) Ì {x } È ens(a).
Exercice 30   Démontrer la correction de ce programme sans utiliser d'ensembles. Indication: on peut se servir du prédicat prem(x,a) = (a ¹ null Þ inserer(x,a).val = x Ú inserer(x,a).val = a.val).

5.6 Terminaison et correction totale

La méthode des assertions ne montre que la correction partielle d'un programme. Elle ne traite pas de la terminaison. Pour montrer qu'un programme termine, il faut alors considérer des ordinaux sur les points du programme et vérifier qu'ils baissent à chaque passage dans un espace bien-fondé, c'est-à-dire ne contenant pas de chaîne infinie décroissante. Reprenons l'exemple de la fonction de Fibonacci, on considère alors les assertions et ordinaux suivants:
static int fibonacci (int n) {
  {n ³ 0}
  int x = 0;
  if (n != 0) {
    x = 1; int y = 0;
    int k = 1;
    {W(n,k) = n - k Ù n ³ k}
    while (k != n) {
      int t = y;
      y = x;
      x = x + t;
      ++k;
    }
  }
  {x = fib(n)}
  return x;
}

A chaque itération, on considère l'ordinal W(n, k) = n-k toujours positif puisqu'on peut vérifier qu'on a toujours n ³ k à ce point du programme. En un tour de boucle, la paire (n,k) devient (n,k+1) et on a donc W(n,k) = n-k > n-k-1=W(n,k+1). Ce programme termine puisque l'ordinal finit par atteindre 0 après un nombre fini d'itérations.

Considérons le programme du PGCD. Un raisonnement analogue consiste à définir l'ordinal W(x,y) = max(x,y). Ici encore, en un tour de boucle, si x>y, on a W(x,y) = max(x,y) > max(x-y,y) = W(x-y,y). De même, si x < y, on a W(x,y) = max(x,y) > max(x,y-x)=W(x,y-x). Par ailleurs W(x,y) est toujours positif, puisque l'invariant x>0 Ù y>0 est maintenu à ce point du programme. Le programme s'arrête donc. On peut remarquer que ce raisonnement s'appuie sur le fait que x et y sont strictement positifs.
static int pgcd (int a, int b) {
  {a > 0 Ù b > 0}
  int x = a, y = b;
  {x > 0 Ù y>0 Ù W(x,y) = max(x,y)}
  while (x != y)
    if (x > y)
      x = x - y;
    else
      y = x - y;
  return x;
}

Exercice 31   Montrer la terminaison de l'algorithme d'Euclide.

Mais les relations d'ordre considérées peuvent dépasser le simple cas de l'inégalité sur les entiers naturels. Plus généralement, si une relation d'ordre (strict) < est toute relation binaire, irréflexive et transitive, c'est-à-dire vérifiant
(i)     ¬ (x < x)
(ii)     x < y < z Þ x < z
On dit qu'elle est bien-fondée s'il n'existe pas de chaîne infinie descendante x0 > x1 > x2 > ··· xn > ···. Quelques exemples d'ordres bien-fondés sont les entiers naturels avec l'ordre sur les entiers á N, < ñ, le produit cartésien d'entiers avec l'ordre lexicographique á N×N, <lñ, ou le produit cartésien d'entiers avec l'ordre sur les multi-ensembles. á N×N, <m ñ où:
(x, y) <l(x',y') si x<x'  Ú  (x=x' Ù y<y')
(x, y) <m (x',y') si (x1,y1) <l(x1',y1')
où (x1,y1) et (x1',y1') sont (x,y) et (x',y') en ordre décroissant (x1 ³ y1, x1' ³ y1'). Par exemple, on a (4,3) >l(4,2) >l(3,15) >l(3, 6) >l(3,4) >l(3,2) >l(2, 21) ... et (2,9) >m (8,7) >m (8,6) >m (7,7) >m (4,6) >m (5,4) >m (5,2) ... .

Ainsi on peut démontrer la terminaison de la fonction d'Ackermann (ci-dessous). En effet, on considère la paire (m,n) des arguments munie de l'ordre lexicographique <l. Alors pour tout m et n (m ³ 0, n ³ 0), la paire (m,n) des arguments décroit strictement dans les appels récursifs. En effet (m,n) >l(m, n-1) et (m,n) >l(m-1, p) pour tout p. Voici un exemple d'ordinaux engendrés par ack(2,3), montrant que l'ordre lexicographique est une méthode assez puissante de démonstration de terminaison: (2, 3), (2, 2), (2, 1), (2, 0), (1, 1), (1, 0), (0, 1), (0, 2), (1, 3), (1, 2), (1, 1), (1, 0), (0, 1), (0, 2), (0, 3), (0, 4), (1, 5), (1, 4), (1, 3), (1, 2), (1, 1), (1, 0), (0, 1), (0, 2), (0, 3), (0, 4), (0, 5), (0, 6), (1, 7), (1, 6), (1, 5), (1, 4), (1, 3), (1, 2), (1, 1), (1, 0), (0, 1), (0, 2), (0, 3), (0, 4), (0, 5), (0, 6), (0, 7), (0, 8).
static int ack (int m, int n) {
  {m ³ 0 Ù n ³ 0 Ù W(m,n) = (m,n)}
  if (m == 0)
    return n + 1;
  else
    if (n == 0)
      return ack (m - 1, 1);
    else
      return ack (m - 1, ack (m, n - 1));
}

Exercice 32   Prouver la terminaison de la fonction 91 de McCarthy définie par:
static int f (int x) {
  if (x > 100)
    return x-10;
  else
    return f(f(x+11));
}

Précédent Remonter Suivant