| | | 3 Exemple | Table des matières |
Dans ce paragraphe, nous présentons un exemple un peu plus conséquent de classe Java spécifiée en JML.
Dans cet exemple, on cherche à spécifier et à programmer des listes d'entiers.
Pour spécifier les listes d'entiers, on définit une interface
Liste qui contient les opérations qui nous intéressent,
accompagnées de leur spécification en JML.
On écrit pour cela le fichier Liste.java suivant.
/**
* Interface pour des listes d'entiers.
*/
public interface Liste {
/**
* Retourne vrai ssi la liste est vide.
*/
/*@ pure */
boolean estVide() ;
/**
* Retourne la taille de la liste.
*
* <pre><jml>
*
* ensures
* \result >= 0 ;
*
* </jml></pre>
*/
/*@ pure */
int taille() ;
/**
* Retourne le i-ème élément de la liste.
*
* <pre><jml>
*
* requires
* 1 <= i && i <= taille() ;
*
* </jml></pre>
*/
/*@ pure */
int element(int i) ;
/**
* Ajoute l'entier val en tête de liste.
*
* <pre><jml>
*
* ensures
* taille() == \old(taille()) + 1 ;
*
* ensures
* element(1) == val ;
*
* ensures
* (\forall int i ;
* 1 <= i && i <= \old(taille()) ;
* element(i + 1) == \old(element(i))) ;
*
* </jml></pre>
*/
void add(int val) ;
/**
* Retourne vrai ssi la liste contient l'élément val.
*
* <pre><jml>
*
* ensures
* \result <==>
* (\exists int i ;
* 1 <= i && i <= taille() ;
* element(i) == val) ;
*
* </jml></pre>
*/
/*@ pure */
public boolean contient(int val) ;
}
La post-condition associée à la méthode taille assure
que la taille est toujours positive. Dans une assertion JML
associée à une méthode, \result représente
le résultat retourné par la méthode.
La pré-condition associée à la méthode element
exige que le paramètre i de cette méthode soit
dans l'intervalle [1, taille()].
La méthode element n'a pas de post-condition explicite ;
on aurait pu écrire de manière équivalente
ensures true ;
La méthode add a trois post-conditions. La première
post-condition exprime que la taille de la séquence augmente d'une unité.
La seconde post-condition exprime qu'après l'appel à add,
le premier élément de la séquence est l'élément ajouté en tête de séquence.
La troisième post-condition exprime que tous les éléments de la séquence
ont été décalé d'un rang vers les indices supérieurs.
La construction
(\forall int i ;
exp1 <= i && i <= exp2 ; condition)
i compris entre exp1 et exp2,
condition est vrai.
La méthode contient a une post-condition qui exprime que
le résultat de l'appel est vrai si et seulement si il existe
un entier i tel que le i-ème élément de la séquence
est égal au paramètre.
La construction
(\exists int i ;
exp1 <= i && i <= exp2 ; condition)
i compris entre exp1 et exp2
tel que condition est vrai.
On peut remarquer qu'on a spécifié les méthodes add et
contient en utilisant les méthodes taille et element,
qui sont purement fonctionnelles (pure).
On implémente l'interface Liste avec une classe
Sequence
On choisit de coder une séquence par un tableau d'entiers. On écrit
le fichier Sequence.java suivant.
/**
* Classe des séquences d'entiers.
*/
public class Sequence implements Liste {
// Une séquence est codée par un tableau d'entiers.
private int[] tableau ;
// Nombre d'éléments de cette séquence
private int taille ;
/**
* Constructeur.
*/
public Sequence() {
tableau = new int[10] ;
taille = 0 ;
}
/**
* Retourne vrai ssi la séquence est vide.
*/
public boolean estVide() {
return taille == 0 ;
}
/**
* Retourne la taille de la séquence.
*/
public int taille() {
return taille ;
}
/**
* Retourne le i-ème élément de la séquence.
*/
public int element(int i) {
return tableau[taille - i] ;
}
/**
* Ajoute l'entier val en tête de séquence.
*/
public void add(int val) {
// On ajoute val à l'indice taille
tableau[taille] = val ;
taille++ ;
}
/**
* Retourne vrai ssi la séquence contient l'élément val.
*/
public boolean contient(int val) {
boolean trouve = false ;
int i = 1 ;
while (i < taille && !trouve) {
trouve = (tableau[i] == val) ;
i++ ;
}
return trouve ;
}
}
Remarques
Liste, on peut spécifier
les opérations sur les séquences directement dans le
fichier Sequence.java. L'intérêt d'utiliser une interface
est qu'on peut implémenter les listes de plusieurs façons
différentes, en créant plusieurs classes qui, comme
Sequence, implémentent l'interface Liste.
Sequence.jml
qui contiendrait la spécification des différentes opérations
et remplacerait l'interface Liste.
Pour tester la classe Sequence, on doit la compiler
avec les assertions JML correspondantes.
Pour cela, on compile les fichiers avec le compilateur JML :
jmlc Liste.java Sequence.java
On écrit ensuite le petit programme de test suivant.
/**
* Un petit programme de test pour les séquences.
*/
class Test1 {
public static void main(String[] args) {
Sequence s = new Sequence() ;
s.add(10) ;
System.out.println("Premier element : " + s.element(1) + "\n") ;
System.out.println("Deuxieme element " + s.element(2)) ;
}
}
L'exécution de ce programme produit la sortie suivante :
Premier element : 10
Exception in thread "main"
org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError:
By method "element" of class "Sequence" for assertions specified at
Liste.java:35:10, when
'i' is 2
'this' is Sequence@2b6651
at Sequence.checkPre$element$Sequence(Sequence.java:847)
at Sequence.element(Sequence.java:946)
at Test1.main(Test1.java:10)
L'affichage du premier élément de la séquence se passe
correctement. Ensuite, on cherche à afficher le deuxième
élément, alors que la séquence n'en comporte qu'un seul.
La pré-condition de element est donc violée, et
l'exception JMLEntryPreconditionError est levée.
Le fichier contenant l'assertion non vérifiée
et les numéros de ligne et de colonne correspondants sont affichés :
Liste.java:35:10.
On retrouve également le numéro de ligne de
l'appel qui a provoqué l'erreur :
Test1.java:10.
On peut remarquer que les numéros de lignes
de programme dans le fichier Sequence sont incorrects.
Cela provient du fait que le compilateur JML
produit un fichier Java qui remplace Sequence.java.
Les numéros de lignes qui sont ensuite affichés
correspondent à ce fichier temporaire.
Pour revenir au programme Test1, l'exception levée
est JMLEntryPreconditionError, ce qui signifie qu'un
appel à la méthode element du fichier de test
viole la pré-condition. Cela met donc en évidence
une erreur dans le fichier de test, et non une erreur
dans la classe Sequence.
Par contre, toute autre exception JML levée indiquerait
une erreur dans la classe Sequence.
| | | 3 Exemple | Table des matières |