Vérification de contraintes OCL avec USE

Dans ce TP nous allons écrire et vérifier des contraintes OCL sur un modèle UML, en nous inspirant de ce que nous avons vu en cours et en TD.

Nous allons utiliser l'outil USE : a UML based Specification Environnement. USE est un outil permettant de définir des diagrammes de classes UML, des diagrammes d'instances conformes à ces diagrammes de classes et de vérifier des contraintes OCL sur ces instances.

Interface de USE

Au lancement de USE, l'interface de l'outil est composée à la fois d'une interface graphique et d'une interface en ligne de commande. Ces deux interfaces permettent de manipuler les mêmes diagrammes chargés par l'outil. L'interface graphique est la suivante :

Eléments numérotés sur l'interface :

1. Bouton qui ouvre une fenêtre permettant d'entrer et évaluer une expression OCL sur les diagrammes (note: on n'utilisera pas directement cette fonctionnalité dans le TP).
2. Affiche et édite le diagramme de classes.
3. Affiche et édite le diagramme d'instances.
4. Evalue les contraintes OCL associées au diagramme de classes sur les instances.
5. Représentation sous forme d'arbre des élements du diagramme de classes, y compris les invariants et les pré/post-conditions sur les opérations.
6. Représentation graphique du diagramme de classes.
7. Représentation graphique du diagramme d'instances.
8. Résultat d'évaluation des invariants OCL. En double-cliquant sur une des lignes, on ouvre une fenêtre affichant l'arbre d'évaluation de l'invariant sur les instances et permettant alors de savoir où se situe le non respect des contraintes.
9. Fenêtre de log où sont notamment affichés les résultats de l'évaluation de la structure (respect des multiplicités sur les associations entre les instances).
10. Affiche la liste de commandes à exécuter pour créer le diagramme d'instances courant. Pour sauvegarder cette liste, passer par le menu principal : File -> Save script.

Actions que l'on peut lancer depuis le menu principal :

• State -> Check structure now : vérifie que les contraintes structurelles sont respectées par les instances.
• State -> Create object : crèe une nouvelle instance d'une classe.

Fichiers utilisables par USE

USE manipule trois types de fichiers :

• ".use" : fichier contenant la description d'un diagramme de classes via une syntaxe textuelle. On y place également les contraintes OCL (invariants et pré/post-conditions) complétant le diagramme de classes.
• ".soil" : fichier qui contient des scripts de création d'objets. Ces scripts sont utiles pour sauvegarder un diagramme d'instances avec les associations entre les instances. En effet, quand on recharge une spécification USE (typiquement quand on a modifié les contraintes OCL), on perd le diagramme d'instances. Il est pratique de le sauvegarder en l'état puis de le recharger directement pour revérifier les invariants OCL.
• ".clt" : il s'agit d'une mise en forme d'un diagramme de classes.

Contraintes OCL

USE intègre toutes les constructions du langage OCL, à l'exception des let ... in et def. On peut néanmoins contourner facilement le fait de ne pas pouvoir définir des attributs globaux et des fonctions OCL via un def en définissant le corps d'une opération d'une classe via une requête OCL, comme permet de le faire USE.

L'évaluation d'invariants OCL sur le diagramme d'instance courant se fait via le bouton 4 sur l'interface.

L'évaluation de pré et post-conditions est plus compliquée car les opérations ne sont pas implémentées dans l'outil, on ne peut donc pas les exécuter réellement. USE permet de simuler leur exécution, via 3 étapes :

1. Entrée dans l'opération : les préconditions associées sont alors vérifiées.
2. Modification manuelle du diagramme d'instance (modificaton de valeurs d'attributs, création ou suppression d'éléments, création ou suppression d'associations ...)
3. Sortie de l'opération : les post-conditions sont alors vérifiées

Les instructions pour entrer et sortir dans une opération sont les suivantes, à exécuter en ligne de commande :

!openter nomObj nomOp([param])
!opexit nomObj [valeurDeSortieAttendue]

Exemples de validation de pré/post-conditions

On dispose d'une classe Compte avec un attribut solde, une opération debiter et une opération getSolde spécifiées de la façon suivante :

context Compte::debiter(somme : Integer)
pre sommePositive: somme > 0
post debitCorrect: self.solde = self.solde@pre - somme

context Compte::getSolde() : Integer
post soldeCorrect: result = solde

Supposons que l'on ait créé un objet nommé monCompte, instance de la classe Compte, et que son solde soit de 1000. Voici ce que donne plusieurs simulations de l'exécution d'opérations :

use> !openter monCompte getSolde()
use> !opexit 1000
postcondition `soldeCorrect' is true

use> !openter monCompte getSolde()
use> !opexit 2000
postcondition `soldeCorrect' is false
evaluation results:
  result : Integer = 2000
  self : Compte = @monCompte
  self.solde : Integer = 1000
  (result = self.solde) : Boolean = false

use> !openter monCompte debiter(100)
precondition `sommePositive' is true
use> !set monCompte.solde := 900
use> !opexit
postcondition `debitCorrect' is true

use> !openter monCompte debiter(-100)
precondition `sommePositive' is false

use> !openter monCompte debiter(100)
precondition `sommePositive' is true
use> !set monCompte.solde := 3000
use> !opexit
postcondition `debitCorrect' is false
evaluation results:
  self : Compte = @monCompte
  self.solde : Integer = 3000
  self : Compte = @monCompte
  self.solde@pre : Integer = 900
  somme : Integer = 100
  (self.solde@pre - somme) : Integer = 800
  (self.solde = (self.solde@pre - somme)) : Boolean = false

Pour plus d'infos :

• USE Quick Tour
• Validation de pré/post-conditions
• Documentation complète

Partie 1 : contraintes sur les personnes

1. Placez les fichiers personnes.use, listePersonnes.soil et personnes.clt dans un répertoire puis lancez USE dans un terminal à partir de ce répertoire. Chargez alors le diagramme de classe UML et les instances associées, contenus dans ces fichiers, via les commandes suivantes :
   

   use> open personnes.use
   use> open listePersonnes.soil
   

2. Affichez le diagramme de classes et via le menu contextuel, chargez la mise en forme avec Load layout en sélectionnant le fichier "personnes.clt".
3. Ouvrez le fichier "personnes.use" avec un éditeur de texte et étudiez le contenu des opérations "getConjoint" et "pasDansMesAncetres" de la classe "Personne" ainsi que la liste des invariants se trouvant à la fin du fichier.
4. Affichez le diagramme d'instances et ajoutez sur les instances existantes des relations de mariage et parents/enfants afin de tester les contraintes OCL associées à ces relations.
   
   Pour rajouter une relation entre deux objets, il faut sélectionner le premier en cliquant dessus puis cliquer sur le deuxième en maintenant la touche Shift enfoncée et via le menu contextuel chosir insert into ... parmi la liste des associations possibles.
5. Certaines contraintes sont manquantes, rajoutez-les comme vu en cours et en TD. Par exemple, il faut vérifier qu'un enfant est plus jeune que ses parents ou qu'on ne peut pas se marier avec ses frères ou ses soeurs.
   
   Pour rajouter des invariants, il faut modifier le ficher "personnes.use" avec un éditeur de texte. Ensuite il faut recharger la spécification. Comme cela supprime le diagramme d'instances, pensez à le sauvegarder en l'état pour le recharger facilement après avoir recharger la spécification.

Partie 2 : contraintes sur les relations entre plusieurs classes

Le diagramme de classes du fichier personnes.use définit plusieurs classes, en plus de la classe Personne, avec les relations suivantes :

• Classe Compte : un compte bancaire pour une personne
• Classe Entreprise : plusieurs employés peuvent travailler pour la même entreprise. Pour simplifier, tous les employés ont le même salaire.
• Pour une entreprise, les salaires sont versés sur le compte bancaire de chacun des employés lorsque l'opération payerSalaire() est appelée. Les salaires payés sont retranchés du budget de l'entreprise, qui doit toujours rester positif.
• Une personne travaille au plus pour une entreprise et possède au plus un compte bancaire. On doit posséder un compte bancaire pour travailler pour une entreprise. On ne peut pas travailler si on a moins de 18 ans.
• Le triplet compte/entreprise/personne doit être cohérent : le compte bancaire d'une personne travaillant pour une entreprise doit appartenir à l'ensemble des comptes bancaires associés à cette entreprise et un compte associé à une entreprise est associé à une personne travaillant pour cette entreprise.

Intégrez les contraintes OCL (invariants et pré/post-conditions d'opérations) pour que cette spécification soit respectée. Vérifiez que vos contraintes sont valides en vous basant par exemple sur le diagramme d'instance du fichier personnesEntreprises.soil.