Logique de Hoare mécanisée
par Jean-Christophe Filliâtre et François Pottier

 Login :  Mot de passe :

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 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 sont utilisés pour montrer la validité de ces formules.

Les outils

Ce TD nécessite des outils qui ont été installés en salles infos. (Si vous souhaitez vraiment travailler sur votre portable ou à distance, le plus simple est certainement de vous connecter sur l'une des machines des salles infos par ssh. L'installation de certains des logiciels nécessaires est fastidieuse et d'autres ne tournent pas sous Windows.)

Vous pouvez éditer les fichiers Java de la manière habituelle (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 le répertoire contenant les sources Java de ce TD (typiquement, le sous-répertoire TD11 de votre workspace Eclipse). Effectuez alors la commande suivante : 

export PATH=/users/profs/info/filliatre/bin:$PATH

Utilisation

La première étape consiste à annoter les programmes Java par des spécifications formelles. 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 et une autre pour indiquer que les preuves de terminaison sont optionnelles : 
//@+ CheckArithOverflow = no
//@+ TerminationPolicy  = user

class Min {
    ...
Attention : lors d'un copy-paste depuis ce sujet, Eclipse ajoute parfois un caractère espace avant le caractère @, ce qui désactive l'annotation correspondante. Pensez à rectifier si besoin.

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 postconditions. 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 clé 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 (partielle) pour getMin peut être 

  //@ 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 ::=  == | != | < | <= | > | >=
Les priorités des connectives logiques sont, de la plus forte à la plus faible : les relations (rel), la conjonction (&&), la disjonction (||), l'implication (==>), l'équivalence (<==>), et la quantification universelle (\forall).

Annotation des boucles

Comme expliqué en cours, 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
//@+ TerminationPolicy = user

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;
    }

}

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 : 
td-hoare 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 (les prouveurs Alt-Ergo, Simplify, Z3, Yices et CVC3 sont installés en salles infos). Le résultat sur chaque obligation est signalé par une icône :

Dans ce TD on adopte la stratégie suivante : chaque obligation doit être validée par au moins un prouveur, quel qu'il soit. Note : on évitera de lancer plusieurs prouveurs en parallèle.

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

Exercices

On commence par quelques exercices d'annotation de boucles. On écrira chaque exercice dans un fichier source différent de la forme 
//@+ CheckArithOverflow = no
//@+ TerminationPolicy  = user

class Exercice {
    ...
}
  1. 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++;
}
  2. 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;
}
  3. 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.

Déposer vos fichiers sources.

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
//@+ TerminationPolicy = user

/*@ 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.

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 c'est un indice où t contient v

Effectuer la vérification.

Complétude

On s'intéresse maintenant à la complétude de cet algorithme. 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.

De même, renforcer la postcondition pour exprimer la complétude de ce programme :

si la valeur renvoyée est positive ou nulle, alors c'est un indice où t contient v; si la valeur renvoyée vaut -1, alors v n'apparaît pas dans t; et ce sont les deux seuls cas possibles

Si l'on utilise une conjonction d'implications, on prendra soin de parenthéser correctement (la conjonction a priorité vis-à-vis de l'implication).

Adapter en conséquence l'invariant de boucle et relancer le processus de 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).

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

Déposer votre fichier source.

Tri par insertion

On se propose maintenant de vérifier la correction (partielle) d'un algorithme de tri. Il s'agit ici d'un algorithme de tri par insertion d'un tableau de n entiers. Le code Java, très simple, est le suivant : 
public class TriParInsertion {

  public static void insertion (int[] t, int i)
  {
    int j, x, y;
    j = i;
    x = t[j];
    while (j > 0 && (y = t[j-1]) > x)
      t[j--] = y;
    t[j] = x;
  }

  public static void tri (int[] t)
  {
    for (int i = 0; i < t.length; i++)
      insertion(t, i);
  }

}
On pourra travailler avec //@+ CheckArithOverflow = no, et passer à yes après que tout fonctionne.

Absence d'erreur à l'exécution

On souhaite d'abord vérifier que le code ci-dessus termine et n'effectue pas d'accès incorrect à la mémoire. On rappelle qu'un accès à t[i] échoue si le pointeur t est nul ou si l'indice i est en dehors des bornes du tableau t.

Dotez les méthodes insertion et tri d'une pré-condition, et dotez chacune des deux boucles d'un invariant, afin de permettre à la machine de vérifier que tous les accès à la mémoire sont sûrs. (Suggestion : exigez que t soit non nul et indiquez à quels intervalles appartiennent les indices i et j.) Dotez ensuite chacune des deux boucles d'un variant, afin de permettre à la machine de vérifier que l'algorithme termine. Cela fait, toutes les obligations de preuve doivent être vérifiées par le prouveur automatique : les témoins doivent être verts.

Vérification du bon ordonnancement

Afin d'éviter la répétition fastidieuse de formules logiques un peu lourdes, on se donne quelques abréviations : 
/*@ predicate trie{Here}(int[] t, integer lo, integer hi) =
  @   \forall integer i, integer j; lo <= i <= j < hi ==> t[i] <= t[j] ;
  @*/

/*@ predicate minore{Here}(int[] t, integer lo, integer hi, integer x) =
  @   \forall integer i; lo <= i < hi ==> x < t[i] ;
  @*/

/*@ predicate majore{Here}(int[] t, integer lo, integer hi, integer x) =
  @   \forall integer i; lo <= i < hi ==> x >= t[i] ;
  @*/

/*@ predicate trie_sauf_trou{Here}(int[] t, integer lo, integer hi,
  @                                integer trou) =
  @   \forall integer i, integer j;
  @   (lo <= i <= j < hi && i != trou && j != trou) ==> t[i] <= t[j] ;
  @*/
(Vous reporterez ces définitions en tête de votre fichier Java.) La signification informelle de ces prédicats est la suivante. La formule trie(t, lo, hi) signifie que la partie du tableau t comprise entre les indices lo inclus et hi exclus est triée. La formule minore(t, lo, hi, x) signifie que la valeur x minore au sens strict cette même partie du tableau. La formule majore(t, lo, hi, x) signifie que x majore au sens large cette même partie du tableau. Enfin la formule trie_sauf_trou indique qu'une partie du tableau est triée, sauf en un point particulier.

On souhaite maintenant vérifier que, à l'issue de la méthode tri, le contenu du tableau t est trié. En d'autres termes, on souhaite attribuer à la méthode tri la spécification suivante : 

  /*@ requires t != null ;
    @ ensures  trie(t, 0, t.length) ;
    @*/
  public static void tri (int[] t)

De façon analogue, proposer une spécification, sous forme de pré- et post-conditions, pour la méthode insertion.

Enrichir les deux invariants de boucle de façon à ce que toutes les obligations de preuve soient satisfaites : les témoins doivent être verts. (Suggestions : dans insertion comme dans tri, indiquez quelles portions du tableau sont triées ; de plus, dans insertion, indiquez où se situe la valeur x vis-à-vis des deux portions triées, et comment les deux portions triées se situent l'une vis-à-vis de l'autre.)

Question subsidiaire

Le résultat obtenu est intéressant, mais ne donne pas la garantie d'avoir correctement implémenté un algorithme de tri. Pourquoi ? Pouvez-vous suggérer quel algorithme clairement incorrect satisferait notre spécification de tri ? Pouvez-vous suggérer comment on devrait renforcer la spécification pour avoir la certitude d'avoir implémenté un véritable tri ?

Déposer votre fichier source.