2 JML

2 JML

JML (Java Modeling Language) a été conçu par Gary Leavens et ses collègues à l'Université de l'Iowa (Iowa State University) [LBR03], [LPC⁺03]. Plusieurs équipes continuent à travailler actuellement sur la conception de JML et sur des outils autour de JML [BCC⁺03].

JML est un langage de spécification pour Java, qui permet de spécifier différentes assertions :

des invariants pour des classes ;
des pré- et des post-conditions pour des méthodes ;
des assertions au milieu de code Java.

JML est un langage inspiré des assertions Eiffel, et des langages de spécifications orientés modèles VDM et Larch.

2.1 Assertions JML

Des assertions JML portant sur un programme Java peuvent être incluses dans ce programme Java, sous l'une des trois formes de commentaires spéciaux suivantes :


   /** 
    * <pre><jml> 
    *
    * invariant condition ; 
    *
    * </jml></pre>
    */ 

   /*@ invariant condition ; */ 

   //@ invariant condition ;

Les conditions sont écrites en Java, sous forme d'expressions booléennes. Ces expressions doivent être purement fonctionnelles, c'est-à-dire sans effet de bord.

On peut spécifier qu'une méthode Java est purement fonctionnelle en plaçant l'assertion

/*@ pure */

juste avant le code de cette méthode. Cette méthode peut alors être utilisée dans des assertions JML.

Les assertions JML peuvent également être définies dans un fichier spécial portant l'extension .jml.

JML utilise la notion d'état visible. Un état visible est un état du système avant ou après l'exécution d'une méthode. Les assertions JML doivent être vérifiées dans un état visible, et non à un point quelconque du programme.

2.2 Assertions associées à des classes

À une classe Java peuvent être associés des invariants et des contraintes d'historique.

Invariant

Un invariant est une condition qui porte sur les attributs de la classe et qui doit être vérifiée dans tout état visible.

Comme en Java, on distingue en JML les invariants d'instance et les invariants de classe. Les invariants de classe sont préfixés par le mot réservé static et ne peuvent faire référence qu'à des constituants de classe (attributs et méthodes static).

Comme les attributs et méthodes en Java, un invariant peut en JML avoir plusieurs niveaux de visibilité : public (public), protégé (protected), paquetage (visibilité par défaut), et privé (private).

Un invariant public peut uniquement faire référence à des constituants publics de la classe.
Un invariant protégé peut uniquement faire référence à des constituants publics et protégés de la classe.
Un invariant ayant la visibilité par défaut ne peut pas faire référence à des constituants privés de la classe.
Un invariant privé peut faire référence à tous les constituants de la classe.

Contrainte d'historique

Une contrainte d'historique permet de poser une condition d'évolution. Il s'agit d'une condition qui porte sur l'état avant l'appel d'une méthode quelconque et l'état après l'appel de cette méthode. On peut faire référence à une expression exp évaluée dans l'état avant l'appel de la méthode avec la construction :

\old(exp)

Comme pour les invariants, on distingue les contraintes d'historique de classe, préfixées par static, qui ne font référence qu'à des constituants de classe, et les contraintes d'historique d'instance.

Comme pour les invariants, on distingue quatre niveaux de visibilité pour les contraintes d'historique : public (public), protégé (protected), paquetage (visibilité par défaut), et privé (private).

Exemple

On peut par exemple définir une classe Compteur comme suit.


class Compteur {

   /**
    * <pre><jml>
    *
    * private invariant val >= 0 ;
    *
    * private constraint val >= \old(val) ;
    *
    * </jml></pre>
    */

   // Valeur du compteur
   private int val ;

   ...
}

La classe Compteur comporte un invariant et une contrainte d'historique. L'invariant

private invariant val >= 0 ;

spécifie que la valeur du compteur doit toujours être positive ou nulle.

Il s'agit d'un invariant d'instance privé car il porte sur l'attribut val qui est un attribut d'instance privé.

La contrainte d'historique

private constraint val >= \old(val) ;

spécifie qu'aucune méthode ne peut faire diminuer la valeur du compteur.

Il s'agit d'une contrainte d'historique d'instance privée car elle porte sur l'attribut val qui est un attribut d'instance privé.

2.3 Assertions associées à des méthodes

À une méthode peuvent être associées des pré-conditions, des post-conditions et des post-conditions exceptionnelles.

Pré-condition

Une pré-condition pour une méthode est une condition portant sur

l'état de l'objet qui invoque la méthode,
les paramètres de la méthode,

qui doit être satisfaite avant chaque appel de cette méthode.

Une pré-condition est introduite en JML par pre ou requires (les deux mots clés sont équivalents).

Post-condition

Une post-condition pour une méthode est une condition portant sur

l'état de l'objet avant l'exécution de la méthode,
l'état de l'objet après l'exécution de la méthode,
les paramètres de la méthode,
le résultat de la méthode,

qui doit être satisfaite après chaque appel de cette méthode qui termine normalement, c'est-à-dire dans lever d'exception.

Une post-condition est introduite en JML par post ou ensures (les deux mots clés sont équivalents).

Post-condition exceptionnelle

Une post-condition exceptionnelle est une condition qui porte sur les mêmes éléments qu'une post-condition, et qui doit être satisfaite après chaque appel de méthode qui termine en levant une exception spécifiée.

Une post-condition exceptionnelle est introduite en JML par signals ou exsures (les deux mots clés sont équivalents).

Exemple

Pour continuer l'exemple précédent, on peut spécifier deux méthodes dans la classe Compteur :

la méthode int getVal() retourne la valeur courante du compteur ;
la méthode void incr(int n) throws Debordement permet d'incrémenter le compteur de n unités. Cette méthode lève l'exception Debordement si la nouvelle valeur est trop grande pour être stockée dans un entier de type int.

On définit l'exception Debordement :


   /**
    * Une exception levée en cas de débordement d'un compteur.
    */

   public class Debordement extends Exception { }

Le code de la méthode getVal() est le suivant :


   /**
    * Retourne la valeur de ce compteur.
    */

   public /*@ pure */ int getVal() {
      return val ;
   }

On spécifie que la méthode getVal() est « pure », ce qui signifie qu'elle n'effectue pas d'effet de bord. Cela permet d'utiliser cette fonction dans une spécification JML, en particulier dans les post-conditions de la méthode incr.


   /**
    * Incrémente la valeur de ce compteur de n.
    *
    * <pre><jml>
    *
    * requires n >= 0 ;
    *
    * ensures getVal() == \old(getVal()) + n ;
    *
    * signals (Debordement deb) getVal() == \old(getVal()) ;
    *
    * </jml></pre>
    */

   public void incr(int n) throws Debordement {
      int nouvelle_valeur = val + n ;
      if (nouvelle_valeur >= 0) {
         val = nouvelle_valeur ;
      } else {
         throw new Debordement() ;
      }
   }

La pré-condition

requires n >= 0 ;

spécifie qu'on ne peut pas incrémenter le compteur d'une valeur négative.

La post-condition

ensures getVal() == \old(getVal()) + n ;

spécifie que si la méthode incr termine normalement (c'est-à-dire sans lever d'exception) alors la valeur du compteur est incrémentée de n.

La post-condition exceptionnelle

signals (Debordement deb) getVal() == \old(getVal()) ;

spécifie que si la méthode incr termine en levant une exception de type Debordement, alors la valeur du compteur n'est pas modifiée.

2.4 Assertions dans le corps des méthodes

Il est possible de placer des assertions JML dans le corps de méthodes Java. Ces assertions sont introduites par le mot clé assert.

Par exemple, on peut ajouter une assertion dans le corps de la méthode incr.


   public void incr(int n) throws Debordement {
      int nouvelle_valeur = val + n ;
      if (nouvelle_valeur >= 0) {
         val = nouvelle_valeur ;
         //@ assert val >= 0 ; 
      } else {
         throw new Debordement() ;
      }
   }

L'assertion

assert val >= 0 ;

spécifie qu'à ce point du programme, l'attribut val est positif ou nul.

2.5 Compilateur JML

Le compilateur JML (jmlc) permet de compiler des classes Java accompagnées de spécifications JML en bytecode Java. Ce compilateur produit, à partir de fichiers Java (extension .java) et de fichiers purement JML (extension .jml) des fichiers en bytecode (extension .class) qui comportent du code qui vérifie à l'exécution les assertions JML.

Pour chaque appel de méthode, les actions suivantes sont (en gros) effectuées :

vérification de la pré-condition de la méthode ;
vérification de l'invariant de la classe ;
appel de la méthode ;
vérification de la post-condition, si la méthode a terminé normalement ; vérification de la post-condition exceptionnelle, si la méthode a terminé en levant une exception spécifiée ;
vérification de l'invariant de la classe ;
vérification de la contrainte d'historique de la classe.

Si une assertion n'est pas vérifiée, une exception spécifique est levée.

La version 3.6 de jmlc définit les exceptions qui peuvent être levée par la vérification des assertions par la hiérarchie de classes suivante :

Les classes en italiques sont des classes abstraites.

On peut remarquer que ces exceptions ne sont pas documentées dans les documents de référence sur JML.

La correspondance entre une assertion non vérifiée et une exception levée est donnée par le tableau suivant :

Assertion non vérifiée	Exception levée
Invariant	JMLInvariantError
Contrainte d'historique	JMLHistoryConstraintError
Pré-condition	JMLEntryPreconditionError
(appel au plus haut niveau)
Pré-condition	JMLInternalPreconditionError
(appel imbriqué)
Post-condition	JMLPostconditionError
Post-condition exceptionnelle	JMLExceptionalPostconditionError
Assertion interne au code	JMLIntraConditionError

On peut remarquer que le compilateur fait une différence entre une pré-condition non vérifiée au plus haut niveau (autrement dit, un appel de méthode situé soit dans le programme principal, soit dans une portion de code qui n'a pas été compilée avec jmlc) et une pré-condition non vérifiée imbriquée (autrement dit, un appel de méthode interne à une autre méthode qui a été compilée avec jmlc).

2 JML

Table des matières