Logique de Hoare mécanisée

par Jean-Christophe Filliâtre et François Pottier (modifé par Stéphane Lengrand)

Ce TD met en œuvre la logique de Hoare sur des programmes Java. On commence par annoter le code source Java par des spécifications formelles ; puis un outil automatique (Why) produit un ensemble de formules logiques, appelées obligations de vérification, exprimant la correction du programme vis-à-vis de cette spécification ; enfin des outils de preuve automatique (par exemple: Alt-Ergo) sont utilisés pour montrer la validité de ces formules.

1. Les outils

Ce TD nécessite des outils qui ont été installés en salles infos.

Vous pouvez éditer les fichiers Java de la manière habituelle (gedit, eclipse, emacs, etc.). Les outils de vérification, en revanche, seront lancés depuis un terminal. Commencez donc par ouvrir un terminal, et placez-vous dans un répertoire de votre choix qui va contenir les fichiers-sources Java de ce TD.

Exécutez la commande gwhy, vous devez avoir comme retour

don't know what to do with

Exécutez alors la commande why-config. Ceci a dû créer dans votre répertoire home les fichiers cachés .whyrc et .gwhyrc.

Utilisation

La première étape consiste à annoter les programmes Java par des spécifications formelles destinées à Why. Les annotations sont insérées sous la forme de commentaires particuliers, de la forme /*@ ... */ ou //@ .... Supposons par exemple que l'on souhaite vérifier le programme suivant calculant le minimum d'un tableau d'entiers :

class Min {
    
    int getMin(int t[]) { 
	int res = t[0];
	for (int i = 1; i < t.length; i++) 
	    if (t[i] < res) res = t[i];
	return res;
    }

}

On commence par ajouter une annotation au debut du fichier pour indiquer que l'on ne souhaite pas (pour l'instant) vérifier l'absence de débordements arithmétiques :

//@+ CheckArithOverflow = no

class Min {
    ...

On peut alors passer à la spécification de la méthode getMin.

Annotation des méthodes

La première forme d'annotation consiste à associer aux méthodes des pré- et post-conditions. Une précondition est une propriété que l'on suppose vraie au moment où la méthode est appelée. Elle est introduite par le mot-clef requires dans une annotation précédant la méthode. Ainsi

  //@ requires t != null && t.length > 0;
  int getMin(int t[]) { ... }

indique que la méthode getMin attend un tableau (non null) ayant au moins un élément. Notez la présence du point-virgule à la fin de l'annotation.

Une postcondition indique au contraire une propriété garantie par la méthode, une fois son exécution terminée. Elle est introduite par le mot clé ensures. Ainsi une postcondition pour getMin peut être par exemple

  //@ ensures \forall integer i; 0 <= i < t.length ==> \result <= t[i];
  int getMin(int t[]) { ... }

Elle exprime que le résultat est plus petit que tout élément de t. Comme on le voit sur cet exemple, la valeur renvoyée par la méthode est dénotée par \result. On notera également que l'on utilise dans la quantification universelle le type integer, qui désigne ici les entiers mathématiques, et non le type int de Java.

Précondition et postcondition sont optionnelles ; lorsqu'elles sont présentes toutes les deux, elles doivent apparaître dans la même annotation, et chacune est terminée par un point-virgule. Ainsi on écrira

   /*@ requires ...;
       ensures ...; */
  int getMin(int t[]) { ... }

Syntaxe des annotations

La syntaxe des formules logiques utilisées dans ces annotations est donnée ci-dessous. Toute expression Java pure, c'est-à-dire sans effet et ne contenant pas d'appel de méthode, peut être utilisée dans une annotation. Les nouveaux opérateurs sont essentiellement l'implication (==>), l'équivalence (<==>) et la quantification universelle (\forall).

    formule ::= expr 
              | expr rel expr 
	      | formule ==> formule 
  	      | formule <==> formule 
 	      | formule && formule 
	      | formule || formule 
	      | \forall type ident ; formule 
        rel ::=  == | != | < | <= | > | >=

Annotation des boucles

La preuve formelle d'un programme nécessite généralement l'annotation de ses boucles par des invariants de boucle. Un invariant de boucle est introduit dans un commentaire précédant la boucle, par le mot clé loop_invariant. Dans l'exemple ci-dessus, un invariant de boucle adéquat est le suivant :

	/*@ loop_invariant 
	  @   1 <= i <= t.length &&
	  @   \forall integer j; 0 <= j < i ==> res <= t[j]; 
	  @*/
	for (int i = 1; i < t.length; i++) 
            ...

Cet invariant exprime d'une part que i reste toujours compris entre 1 et t.length et d'autre part que res est plus petit que toutes les valeurs t[0],...,t[i-1]. Notez qu'il faut écrire i <= t.length et non i < t.length car l'invariant doit être vérifié à la fin de la dernière exécution du corps de la boucle, où i = t.length.

Pour prouver d'autre part la terminaison de cette boucle, il faut spécifier un variant, c'est-à-dire un entier naturel qui décroît à chaque tour de boucle. Ici t.length-i convient :

	/*@ loop_invariant 
	      ...
	  @ loop_variant
	  @   t.length - i;
	  @*/
	for (int i = 1; i < t.length; i++) 
            ...

Notez que l'invariant et le variant doivent être spécifiés à l'intérieur d'un unique commentaire, et que chacun est terminé par un point-virgule.

Le source complètement annoté est donc le suivant :

//@+ CheckArithOverflow = no

class Min {
    
    /*@ requires t != null && t.length > 0;
      @ ensures  \forall integer i; 0 <= i < t.length ==> \result <= t[i];
      @*/
    int getMin(int t[]) { 
	int res = t[0];
	/*@ loop_invariant 
	  @   1 <= i <= t.length &&
	  @   \forall integer j; 0 <= j < i ==> res <= t[j]; 
	  @ loop_variant
	  @   t.length - i;
	  @*/
	for (int i = 1; i < t.length; i++) 
	    if (t[i] < res) res = t[i];
	return res;
    }
    
}

Copiez ce programme dans un fichier Min.java.

Preuve automatique

Une fois le programme annoté, on peut procéder à la vérification. Pour cela, il suffit d'exécuter dans le terminal la commande suivante :

gwhy Min.java &

où Min.java est le fichier source. (Pensez à sauver auparavant votre fichier dans l'éditeur.) Une fenêtre s'ouvre, qui doit ressembler à ceci :

On lance alors les outils de preuve automatique en cliquant sur le sommet de la colonne correspondante (le prouveur Alt-Ergo est installé en salles infos). Le résultat sur chaque obligation est signalé par une icône :

pour une obligation valide ;
pour une absence de réponse du prouveur dans le temps imparti ;
, ou pour un échec du prouveur. Un échec du prouveur ne signifie pas pour autant que l'obligation n'est pas valide (elle pourrait très bien être validée par un autre prouveur).

Lorsqu'une obligation n'est pas prouvée, il y a trois raisons possibles à cela :

le programme est incorrect ; c'est là un cas satisfaisant car c'est finalement le but d'une preuve formelle que de trouver des erreurs dans un programme.
la spécification est incorrecte, i.e. on a incorrectement ou incomplètement spécifié le programme; c'est malheureusement souvent le cas lorsque l'on débute la spécification formelle d'un programme.
le prouveur n'est pas assez puissant ; c'est là presque une fatalité, la logique des prédicats du premier ordre étant indécidable. Dans ce TD, cependant, l'objectif est de parvenir à une preuve 100% automatique. On devra donc se pencher sur les deux premiers cas de figure avant d'envisager que le prouveur est en cause.

Note : il est possible que certaines obligations ne soient pas prouvées car trop peu de temps est donné au prouveur. Il est possible d'allouer plus de temps aux prouveurs en modifiant la durée Timeout apparaissant en bas à gauche de la fenêtre de l'outil (nombre de secondes).

2. Exercices de mise en jambes

On commence par quelques exercices d'annotation de boucles. On écrira chaque exercice dans un fichier source différent de la forme

//@+ CheckArithOverflow = no

class Exercice {
    ...
}

où ... sera remplacé par le code à vérifier.

Prouver la terminaison des deux boucles suivantes :

static void loop1(int n) { 
  //@ loop_variant ...;
  while (n > 0) n--; 
}

static void loop2(int n) { 
  //@ loop_variant ...;
  while (n < 100) n++; 
}

en remplaçant ... par un variant adéquat.

Prouver la correction et la terminaison de la méthode suivante :

//@ ensures \result == 0;
static int loop3() {
    int i = 100;
    //@ loop_invariant ...; loop_variant ...;
    while (i > 0) i--;
    return i;
}

On considère une méthode all_zeros qui prend en argument un tableau d'entiers et détermine si tous ses éléments sont nuls. Le code et sa spécification sont les suivants :
```
/*@ requires t != null;
  @ ensures \result <==> \forall integer i; 0 <= i < t.length ==> t[i]==0; 
  @*/
static boolean all_zeros(int t[]) {
    /*@ loop_invariant ...; 
      @ loop_variant   ...; 
      @*/
    for (int k = 0; k < t.length; k++) if (t[k]!=0) return false;
    return true;
}
```
Donner un invariant et un variant à la boucle for de manière à prouver la correction et la terminaison de ce programme.

3. Recherche dichotomique dans un tableau trié

Nous considérons ici le problème de la recherche dichotomique dans un tableau trié (binary search). Étant donné un tableau t d'entiers, trié par ordre croissant, et une valeur v, on chercher à déterminer si v apparaît dans t. Le tableau étant trié, on peut procéder par dichotomie, en divisant par deux l'espace de recherche à chaque étape. Le programme suivant effectue cette recherche, les variables l et u délimitant l'espace de recherche.

//@+ CheckArithOverflow = no

/*@ lemma mean: \forall integer x y; x <= y ==> x <= (x + y)/2 <= y; */

/*@ lemma div2: \forall integer x y; 0 <= x ==> 0 <= x/2 <= x; */

public class BinarySearch {
    static int binary_search(int t[], int v) {
        int l = 0, u = t.length - 1;
        while (l <= u) {
            int m = (l + u) / 2;
            if (t[m] < v) l = m + 1;
            else if (t[m] > v) u = m - 1;
            else return m; 
        }
        return -1;
    }
}

Les deux lemmes mean et div2 sont là pour aider les prouveurs en ce qui concerne la division par 2 (on ne cherchera pas à faire prouver ces deux lemmes par les prouveurs).

Absence d'erreur à l'exécution

Dans un premier temps, on se contente de montrer que le programme s'exécute correctement i.e.

qu'il ne déréférence pas de pointeur null ;
qu'il n'accède pas au tableau t en dehors de ses bornes ;
qu'il termine.

Pour cela, donner à la méthode binary_search une précondition exprimant que le tableau t n'est pas null et à sa boucle while un invariant de boucle portant sur les indices l et u et un variant.

Correction

On s'intéresse maintenant à la correction de la méthode binary_search.

Donner une spécification formelle à cette méthode, c'est-à-dire une postcondition exprimant

si la valeur renvoyée est positive ou nulle, alors cette valeur est l'indice d'une case de t qui contient v

Lancer Why pour effectuer la vérification.

Complétude

On s'intéresse maintenant à la complétude de cet algorithme.

Renforcer la postcondition pour exprimer la complétude de ce programme :

si la valeur renvoyée est positive ou nulle, alors cette valeur est l'indice d'une case de t qui contient v ;
si la valeur renvoyée vaut -1, alors v n'apparaît pas dans t ;
ce sont les deux seuls cas possibles

La postcondition renforcée contient une conjonction d'implications, que l'on prendra soin de parenthéser correctement (la conjonction a priorité vis-à-vis de l'implication). Que se passe-t-il si vous lancez un prouveur comme Alt-Ergo ?

Précondition

Le comportement observé est normal : à aucun moment nous avons exprimé l'hypothèse que le tableau passé en argument était trié. De fait, s'il ne l'est pas, la méthode est icomplète.

Renforcer la précondition pour exprimer le caractère trié du tableau t :

le tableau t n'est pas null et il est trié par ordre croissant

Note : il existe plusieurs manières de spécifier qu'un tableau est trié. On préférera la forme à deux variables « pour tout i et tout j, si i <= j alors ... » (à la forme utilisant une quantification sur une seule variable), car elle produit des obligations de preuve plus simples, qui ne nécessitent pas de preuve par récurrence.

A nouveau, que se passe-t-il si vous lancez Why et Alt-Ergo ?

Invariant de boucle

L'invariant de boucle est trop faible pour en déduire que la postcondition est valide.

Renforcer l'invariant pour exprimer que :

toute case du tableau t qui contient v a son indice compris entre l et u (au sens large)

Lancer Why pour effectuer la vérification.

Non-dépassement de la capacité des entiers

Enfin, on souhaite montrer qu'il n'y a pas dépassement de la capacité des entiers machines durant l'exécution de ce programme. Pour cela, modifier ainsi la première ligne du fichier

//@+ CheckArithOverflow = yes

et relancer le processus de vérification.

Il doit rester au final une seule obligation de preuve non prouvée. Elle correspond à un problème de dépassement éventuel de la capacité des entiers. Identifier et modifier la ligne correspondante dans le code, et relancer le processus de vérification. (Une fois cette question terminée, on pourra lire avec intérêt cet article).

4. Tri par insertion

On fournit le code suivant du tri par insertion :

class Tri { 
      void tri(int[] t) { 
	for (int i=0; i < t.length; i++){
	    int x = t[i];
	    for(int j=i-1; j >= 0 && t[j] > x; j--){
		t[j+1] = t[j];
		t[j]=x;
	    }
	} 
    }
}

Vérifications de base

Formuler une précondition exprimant le fait que le tableau t est supposé ne pas être le pointeur null et ajouter des variants et des invariants pour montrer, premièrement, la terminaison des boucles et, deuxièmement, que l'on accède jamais à une case du tableau qui n'existe pas.

Les cases ne contiennent pas deux fois la même valeur

Renforcer la precondition pour exprimer le fait que les cases ne contiennent pas deux fois la même valeur.

Donner cette même propriété comme post-condition.

Renforcer les invariants pour montrer la post-condition.

Les cases sont triées

Renforcer la postcondition pour exprimer le fait que les cases se retrouvent triées.

Renforcer les invariants pour montrer la post-condition.

Solution des exercices

C'est ici.