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.
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 TD12 de votre workspace Eclipse). Effectuez alors la commande suivante :
export PATH=/users/profs/info/filliatre/bin:$PATH
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.
//@ 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[]) { ... }
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).
/*@ 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; } }
td-hoare Min.javaoù 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 :
Lorsqu'une obligation n'est pas prouvée, il y a trois raisons possibles à cela :
//@+ CheckArithOverflow = no //@+ TerminationPolicy = user class Exercice { ... }
static void loop1(int n) { //@ loop_variant ...; while (n > 0) n--; } static void loop2(int n) { //@ loop_variant ...; while (n < 100) n++; }
//@ ensures \result == 0; static int loop3() { int i = 100; //@ loop_invariant ...; loop_variant ...; while (i > 0) i--; return i; }
/*@ 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.
//@+ 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).
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.
Effectuer la vérification.
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 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.
//@+ CheckArithOverflow = yeset 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.
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.
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.
/*@ 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.)
Déposer votre fichier source.