CentraleSupélec LRI
Département informatique Équipe MODHEL
3 rue Joliot-Curie Bât 650 Ada Lovelace, Université Paris Sud
F-91192 Gif-sur-Yvette cedex, France Rue Noetzlin, 91190 Gif-sur-Yvette, France
BE de sémantique des langages

L'objectif de ce bureau d'étude est de se familiariser avec la sémantique axiomatique en effectuant la preuve de quelques programmes Java.

Livraison

Livraison sur wdi.supelec.fr/Livraison avec le code 2RGY


Les annotations sémantiques seront écrites en JML (Java Modeling Language), et traitées par l'outil Krakatoa dans Why.

  1. Saisir le programme Produit.java donné en exemple et le vérifier en tapant la commande krakatoa Produit.java dans un terminal. Le prouveur automatique Alt-Ergo doit permettre de valider toutes les obligations de preuve.
    Note : lors du premier lancement de why, les prouveurs disponibles ne sont pas configurés, et vous aurez un message d'erreur. Il suffit d'exécuter la commande why3 config --detect-provers, puis de relancer krakatoa.
  2. Écrire en Java une classe Isqrt munie d'une méthode static calculant la partie entière de la racine carrée d'un entier en utilisant la propriété suivante :{$$n^2=\sum_{i=0}^{n-1}2i+1$$}Ajouter les prérequis, post-condition et invariant en JML pour démontrer que votre code calcule bien cette partie entière. Ajouter un variant pour montrer que le programme termine. Le code Java vous est fourni ci-dessous.
  3. Faire de même avec un programme qui calcule le PGCD de deux entiers par soustractions successives. Il faudra définir un prédicat gcd(integer x, integer y, integer d) qui est vrai lorsque d est le PGCD de x et y. Vous aurez pour cela besoin d'un prédicat divides(integer x, integer y) qui indique si x divise y.
  4. S'il vous reste du temps, utiliser Isabelle pour faire la preuve des lemmes introduits pour le pgcd (l'un d'eux n'est pas prouvé automatiquement), ou faire la preuve du tri par sélection.

Syntaxe JML

Les commentaires spéciaux contenant du JML sont de la forme : /*@ <code JML> @*/ ou //@ <code JML jusqu'en fin de ligne>

Vous ne pouvez mettre qu'un seul prédicat ou un seul lemme dans chaque commentaire spécial.

Les mots-clefs suivants peuvent être utilisés :

requires
pour donner une précondition : requires n >=0 ;
ensures
pour donner une postcondition : ensures \result == n*n ;
loop_invariant
pour donner l'invariant d'une boucle : loop_invariant i+j == n ;
loop_variant
pour donner un variant d'une boucle (valeur qui décroit à chaque tour de boucle et reste positive ou nulle) : loop_variant j - i;
lemma
pour donner un lemme (permet de guider le prouveur) :
  lemma mul_distr_r:
    \forall integer a b c; (a+b)*c == a*c + b*c ;
assert
pour indiquer qu'une propriété est vraie à ce point du programme : assert i > 0 && j > 0 ;
predicate
pour définir un prédicat logique : predicate even(integer n) = n%2 == 0 ;
\result
pour faire référence à la valeur de retour d'une fonction
\old
pour faire référence à la valeur initiale d'une variable dans la postcondition : \old(i)
\at
pour faire référence à la valeur précédente d'une variable un invariant : \at(i,Pre)
\forall
pour le quantificateur universel : \forall integer n; n+1 > n;
\exists
pour le quantificateur d'existence : \exists integer k; 4 == 2*k ;
==>
pour l'implication : \forall integer x; x == 3 ==> x/2 == 1 ;
<==>
pour l'équivalence : \forall integer x; x%2 == 0 <==> x == 2*(x/2) ;
ghost
pour introduire des variables fantômes qui instrumentent le code : ghost integer gx = x ;

Exemple

Ce programme calcule le produit de deux entiers en n'utilisant que la somme, la différence et les décalages arithmétiques à gauche (multiplication par 2) et à droite (division par 2) :

// On désactive la vérification des débordements
//@+ CheckArithOverflow = no
class Produit {
  // La fonction produit(a,n) rend a*n si n est positif ou nul
  /*@
    @ requires n >= 0;
    @ ensures \result == \old(a)*\old(n) ;
    @*/
  public static int produit(int a, int n) {
    // On utilise des variables 'fantômes' pour mémoriser les valeurs initiales
    //@ ghost integer a_init = a;
    //@ ghost integer n_init = n;
    int r = 0;
    // On caractérise la boucle par un invariant (pour la preuve) et un variant (pour la terminaison)
    /*@
      @ loop_invariant r+a*n == a_init*n_init && n >= 0  ;
      @ loop_variant n;
      @*/
    while (n != 0) {
      if (n%2 != 0) {
        n--;
        r += a;
      }
      // On utilise des assertions pour forcer le prouveur à les vérifier et le guider ainsi dans la démonstration
      //@ assert r+a*n == a_init*n_init ;
      //@ assert n%2 == 0 ;
      //@ ghost integer even_n = n ;
      n /= 2;
      //@ assert 2*n == even_n;
      a *= 2;
      //@ assert r+a*n == a_init*n_init ;
    }
    return r;
  }
}

La commande à utiliser pour vérifier ce code Java est : krakatoa Produit.java

Partie entière de la racine carrée d'un entier

//@+ CheckArithOverflow = no

// Lemmes nécessaires pour l'arithmétique non linéaire
/*@ lemma distr_right: 
  @   \forall integer x y z; x*(y+z) == (x*y)+(x*z);
  @*/

/*@ lemma distr_left: 
  @   \forall integer x y z; (x+y)*z == (x*z)+(y*z);
  @*/

// Définition du carré (fonction sqr)
//@ logic integer sqr(integer x) = x * x;

public class Isqrt {
    // Le résultat doit être la partie entière de la racine carrée de x
    public static int isqrt(int x) {
        int count = 0, sum = 1;
        while (sum <= x) { 
            count++;
            sum = sum + 2*count+1;
        }
        return count;
    }   
}

Calcul du pgcd de deux entiers

//@+ CheckArithOverflow = no

public class Pgcd {
  /*@ requires a > 0 && b > 0 ;
    @ ensures is_gcd(a, b, \result);
    @*/
  public static int pgcd(int a, int b) {
    while (a != b) {
      if (a > b) {
        a = a - b;
      } else {
        b = b - a;
      }
    }
    return a;
  }
}