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 TD et TP.

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'instance conformes à ces diagrammes de classe et de vérifier des contraintes OCL sur ces instances.

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.
  2. Affiche et édite le diagramme de classe.
  3. Affiche et édite le diagramme d'instance.
  4. Evalue les contraintes OCL associées au diagramme de classe 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 classe.
  7. Représentation graphique du diagramme d'instance.
  8. Résulat 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'instance courant.

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

Fichiers utilisables par USE

USE manipule deux types principaux de fichiers :

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 :

Partie 1 : contraintes sur les personnes

Placez les fichiers personnes.use, listePersonnes.cmd 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.cmd

Affichez le diagramme de classes (bouton 2) et chargez le fichier personnes.clt via l'option Load Layout du menu contextuel pour utiliser directement une mise en forme lisible du diagramme.

Affichez le diagramme d'instances (bouton 3) et ajoutez sur les instances existantes des relations de mariage et parents/enfants afin de tester les contraintes OCL associées à ces relations. Certaines sont tout de même manquantes, rajoutez-les. Par exemple, il faut vérifier qu'un enfant est plus jeune que ses parents ou qu'on n'est pas marié avec son frère ou sa soeur.

Partie 2 : contraintes sur les relations entre plusieurs classes

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

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.cmd.