Skip to topic | Skip to bottom
Home
Minfo
Minfo.GlooTD4r1.2 - 09 Oct 2007 - 11:40 - PhilippeCollettopic end

Start of topic | Skip to actions

TD 4 : Spécifications et tests en Java : JML et JUnit

PhilippeCollet

Point de départ

  • ALERT! Attention, les fichiers sources qui vous sont donnés utilisent le format ISO-8859 et vos environnements Linux sont par défaut en UTF-8
    • Idéalement, modifiez la variable LANG comme suit (soit avant de lancer Eclipse, soit dans vos fichiers d'environnement) :
export LANG=fr_FR.ISO-8859-1
  • Créez un nouveau projet pour ce 4ème TD.
  • Téléchargez l'archive jmlbebetes.zip et décompactez la dans le répertoire de votre projet, puis rafraichissez les fichiers du projet pour voir apparaitre les nouveaux packages et classes.

Vous êtes encore face à une nouvelle version du simulateur de bébêtes, qui tente de répondre à une partie des tests demandés dans le TD3 :

  • Des cas de test ont été créés pour la méthode effectueDeplacement() afin de détecter et de corriger trois erreurs :
    1. la largeur et la hauteur ont été confondues dans une affectation.
    2. Les modifications sur x et y ne sont pas faites indépendamment (si x doit être modifié, y ne l'était pas, ce qui est gênant dans les coins).
    3. L'opérateur % n'est pas vraiment modulo, c'est le reste de la division entière, donc si la directionCourante devient négative, elle n'est pas modifiée...
  • Le code a donc été modifié dans la méthode effectueDeplacement() et tous les tests fournis passent (cela ne veut pas dire qu'il n'y a pas d'autres erreurs, ni que le code de déplacement fourni est parfait...).

Cette nouvelle version du simulateur fait aussi quelques modifications sur le champ, pour lequel le thread de simulation est maintenant explicitement démarré à l'aide d'une méthode hors du constructeur. TIP Quel impact ? me direz-vous. Cela permet notamment de créer des contextes de test avec un champ sans que le moteur de simulation soit déclenché. Et alors ? me rétorquerez-vous. Et alors, imaginez que le thread du moteur de simulation appelle la méthode agit, donc effectueDeplacement() sur la même bébête à laquelle vous faites un test unitaire, et ce, juste après que vous ayez vous même appeler effectueDeplacement() et juste avant que soient appelées vos fonctions d'oracle. Que risque-t-il de se passer ? oui... Des échecs de test dus au multi-thread !!!

Pour exécuter ce code, il faut encore que notre projet, tout neuf, explicite qu'il a besoin de la bibliothèque de JUnit, junit.jar. Dans le TD3, le fait de passer par les assistants de création de tests avait automatisé cette tâche...

  • Il suffit d'éditer une des classes de test : l'importation du package junit provoque une erreur symbolisée par une icone à gauche de la ligne; en cliquant dessus, la première proposition est d'importer junit 3.8... Et voila !
  • Exécutez les tests pour vérifier que tout fonctionne comme prévu.

Spécifications en JML

Vous pouvez aussi remarquer que certaines parties de classes contiennent quelques spécifications JML (des invariants, quelques pré et postconditions). On va maintenant s'aider de ces spécifications JML pour tester, de différentes manières, certains aspects du simulateur de bébêtes.

ALERT! Remarques préalables sur JML et l'environnement JMLtools 5.4-RC1

  • L'environnement JML que nous utilisons (version 5.4-RC1) supporte le JDK 1.5 (il est capable de s'interfacer avec un compilateur du JDK 1.5), mais pas encore les extensions de syntaxe de Java 5 (généricité, autoboxing, annotations, etc.). Il existe de nouvelles versions de JML, mais qui ne supportent toujours pas la syntaxe Java 5/6 et qui en plus ne disposent plus du pilotage par ant...

  • Dans cette version, le compilateur JML :
    • vérifie par défaut les clauses "assignable"
    • considère que tout attribut déclaré sur une référence de type (hors type de base, donc) est implicitement spécifié "non_null". Pour expliciter le contraire, il faut indiquer que l'attribut est "nullable", comme cela est fait dans la classe ChampDeBebetes.

Configurer votre environnement pour JML

Les outils JML peuvent être utilisés comme des commandes, mais on va les utiliser à travers ant. Vous devez avoir dans votre répertoire un fichier build.xml et les deux fichiers de propriétés. Des cibles et des propriétés ont été ajoutées pour piloter les outils JML. Les hypothèses sur l'environnement sont légèrement modifiées et un répertoire lib à la racine du projet peut maintenant contenir des bibliothèques nécessaires aux projets. Dans le fichier default.properties, des propriétés définissent les différentes bibliothèques nécessaires.

Il faut maintenant configurer votre environnement pour pouvoir utiliser les outils JML :

  • Créez un répertoire lib à la racine de votre projet.
  • Créez des liens symboliques de tous les fichiers du répertoire ~collet/minfo/TD4/lib/ vers le répertoire lib de votre projet (le répertoire contient 2 jars).
  • Dans votre projet Eclipse, vous avez du remarquer que le fichier build.xml contient des erreurs. Plus précisément, des tâches optionnelles JML ne sont pas reconnues car il manque le jar nécessaire dans le chemin de l'outil ant utilisé par Eclipse. Pour réparer cela, allez dans Window/Preferences, une fenêtre apparaît et vous pouvez sélectionner Ant/Runtime dans l'arborescence de droite. Enfin, dans l'onglet Classpath, sélectionnez Global Entries et faites Add external JARs : dans la fenêtre qui apparaît, naviguez jusqu'a sélectionner le fichier jml-release.jar qui se trouve dans le répertoire lib et validez. Ouf ! c'est fait et le fichier build.xml ne devrait plus faire apparaître d'erreur (ALERT! si vous n'y arrivez pas, faites-vous aider, sinon, vous ne pourrez utiliser JML !).
  • Les cibles intéressantes pour JML sont :
    • compileJML : qui compile tous les fichiers Java pour produire un bytecode JML+java (on utilisera cela pour compiler)
    • fullcheckJML : qui vérifie uniquement la cohérence des spécifications JML dans les fichiers sources. Par défaut, cette tâche ant vérifie tous les aspects des spécifications JML.
    • runJML : qui lance l'application en activant les assertions (on utilisera cela pour exécuter)
    • runJMLtest : qui lance des tests avec les assertions JML activées.

Exécution avec les assertions JML

A l'aide d'Eclipse, lancez la tâche ant "runJML" qui va tout compiler (car elle dépend de "compileJML") et lancer l'application avec les assertions activées.

  • Que constatez-vous ?
  • Il faut donc corriger un certain nombres d'erreur dans le code. Faites-le jusqu'a ce qu'aucune assertion ne soit violée à l'exécution.

Il manque un invariant dans la classe BebeteAbstraite pour contraindre la direction courante. Ajoutez le, puis relancer...

  • Continuez à corriger...

Aide : Lorsque vous ajoutez des assertions JML, n'oubliez pas que la syntaxe est bien précise à l'intérieur des commentaires Java (pas d'espace entre le commentaire et @) :

//@ assertion
ou
/*@ assertion1
  @ assertion2
  @*/

ALERT! Remarque : Ici, on n'a vraiment fait des tests unitaires, mais plutot un test d'intégration avec les 10 bébêtes qui se balladent au hasard dans le champ.

Exécution de tests avec les assertions JML

A l'intérieur d'Eclipse, lancez la tâche ant "runJMLtest" qui va lancer tous les tests unitaires avec les assertions activées:

  • Que constatez-vous ?
  • Jetez un coup d'oeil a la racine du projet. Il y a normalement un fichier de résumé par classe de test.
  • Pour corriger les erreurs JML, pensez que le compilateur JML passe aussi sur les classes de tests, donc que les attributs de ces classes doivent être déclarés "nullable" si nécessaires...

A l'aide de l'assistant de création de TestCase, créez un nouvelle classe pour tester le constructeur de ChampDeBebetes. Créez justement un champ de 9 pixels de large et 9 pixels de haut avec 10 bébêtes.

  • Relancez les tests.
  • Trouvez quelle assertion est violée.
  • La source de l'erreur est-elle vraiment dans la classe incriminée ?
  • Placez une ou plusieurs assertions supplémentaires pour contraindre le champ par rapport à la vitesse max.
  • Retestez.
  • Si vous avez bien fait le travail, le test échoue toujours mais pas au même endroit. C'est normalement votre assertion qui détecte le problème. Il faudrait donc que le test passe, ou du moins, qu'il ne soit pas significatif... Pour cela, entourez votre appel au constructeur par le code suivant (il faudra inclure la bibliothèque jmlruntime dans les propriétés de votre projet) :
       try {
            // @TODO : mettre le code du constructeur de champ
            // Pas de code de test, ce sont les assertions qui vont faire le travail d'oracle
        } catch (org.jmlspecs.jmlrac.runtime.JMLPreconditionError e) {
            // devrait être comptabilisé comme "sans signification"
        } catch (org.jmlspecs.jmlrac.runtime.JMLAssertionError e) {
            // vraie erreur, les postconditions ou invariants ne sont pas satisfaits
            fail(e.getMessage());
        }
  • Ce code permet d'effectuer le filtrage entre des tests qui font échouer les préconditions (donc non significatifs) et ceux qui font échouer les postconditions ou les invariants (les vraies erreurs).
  • Retestez et vérifier que tout va bien maintenant !

Pour ceux qui s'ennuient...

  • Trouver les invariants du champ qui doivent être ajoutés pour contraindre ses dimensions en fonction de la taille de la bébête (indice : allez voir la fabrication des bébêtes).
  • Rajoutez des assertions dans les classes des bébêtes et du champ, testez.
  • Ecrivez des tests, testez encore et encore cool!

-- PhilippeCollet - 25 Sep 2007

  • :

to top

You are here: Minfo > GLOO > GlooTD4

to top

Copyright © 1999-2017 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding WIKIDeptinfo? Send feedback