WOW !! MUCH LOVE ! SO WORLD PEACE !
Fond bitcoin pour l'amélioration du site: 1memzGeKS7CB3ECNkzSn2qHwxU6NZoJ8o
  Dogecoin (tips/pourboires): DCLoo9Dd4qECqpMLurdgGnaoqbftj16Nvp


Home | Publier un mémoire | Une page au hasard

 > 

EM-OCL : une extension mathématique d'OCL

( Télécharger le fichier original )
par Houda Trabesli
Ecole d'ingénieurs de Sfax - Tunisie - MAster de recherche 2010
  

précédent sommaire suivant

Bitcoin is a swarm of cyber hornets serving the goddess of wisdom, feeding on the fire of truth, exponentially growing ever smarter, faster, and stronger behind a wall of encrypted energy

Chapitre 1

La conception par contrats en UML/OCL

Introduction

En général, les langages graphiques (comme UML [?]), ne décrivent qu'un aspect partiel du système. Les contraintes sur le modèle sont décrites sous la forme de notes en langage naturel, ce qui induit une ambiguïté de ce dernier et pénalise sa vérification automatique.

Le langage OCL [10](Object Constraint Language) vient remédier àces insuffisances proposant la possibilité à un Classifier donné d'établir ses responsabilités d'une façon précise moyennant un ensemble de propriétés. Dans ce chapitre, nous étudions d'une façon approfondie les aspects généraux d'OCL et donnons un aperçu sur les travaux de recherche récents liés à OCL.

1.1 Généralités sur la conception par contrats

Le fondateur de la conception par contrats (Design by contracts) est Bertrand Meyer auteur du langage de programmation orienté objet pur : Eiffel [6]. Un contrat exige deux partenaires. Dans l'approche par objets, on distingue :

- contrat client basé sur la relation Fournisseur-client (association en UML) entre deux classes; - contrat d'héritage basé sur la relation d'héritage simple (généralisation-spécialisation en UML) entre deux classes.

Afin de définir d'une façon formelle un contrat, on distingue les clauses suivantes : - Précondition : doit être vérifiée avant l'exécution d'une opération ou méthode.

- Postcondition : doit être vérifiée après l'exécution d'une opération ou méthode.

- Invariant: doit être vérifiée en permanence (au moment stable) durant la vie d'un objet (après

sa création).

Pour le contrat client, le protocole à respecter est le suivant :

- précondition est une obligation pour le client et un droit pour le fournisseur. - postcondition est un droit pour le client et une obligation pour le fournisseur. - invariant est un droit pour le client et une obligation pour le fournisseur.

Pour le contrat d'héritage, le protocole à respecter par la classe descendante est : - on peut affaiblir la précondition d'une méthode ou opération héritée.

- on peut renforcer la postcondition d'une méthode ou opération héritée. - on peut renforcer l'invariant venant de la classe ascendante.

1.2 Le langage OCL

OCL est un langage sans effet de bord, fortement typé, s'applique sur les objets et les liens d'un diagramme de classes. C'est un langage fonctionnel, basé sur la logique du premier ordre, navigationnel et déclaratif. OCL est un langage de spécification pas de programmation : haut niveau d'abstraction, pas forcément exécutable. Il permet de trouver des erreurs beaucoup plus tôt dans le cycle de vie. Deux utilisations possibles d'OCL pourront être envisagées :

- OCL pour la conception de contrats;

- OCL en tant que langage de requêtes à l'instar de SQL [17].

1.2.1 OCL langage sans effet de bord

OCL n'a aucune action de modification sur un diagramme d'objets (contrairement au langage SQL qui utilise les constructions insert, update et delete). De même, il n'a aucune action sur le diagramme de classes (contrairement au langage SQL qui peut créer et mettre à jour un schéma relationnel). Toute expression OCL est censée décrire une contrainte ou bien une requête.

1.2.2 OCL est un langage basé sur la logique des prédicats du 1er ordre

OCL utilise deux types de formules. Les formules ouvertes, qui font référence à des objets ou données, sont utilisées à travers les itérateurs (select, reject, ..). Les formules fermées, qui font appel à des quantificateurs et dont le résultat est booléen, sont utilisées à travers les deux opérateurs exists ? et forAll ?.

1.2.3 L'approche fonctionnelle du langage OCL

OCL est un langage fonctionnel

Toute expression OCL retourne un résultat de type : une donnée de base (Boolean, String, Integer,...), ou un objet de l'une des classes du diagramme de classes, ou une collection. Tout interprète retourne deux informations après évaluation d'une expression OCL : le résultat et le type du résultat.

Enchaînement des opérations sur les collections

Toute expression retourne un résultat typé, donc on peut appliquer une opération à ce résultat. Ceci évite l'utilisation des variables intermédiaires.

Syntaxe générale des expressions OCL

Une expression OCL est toujours écrite dans un contexte qui peut être soit un type soit une opération. Si le contexte est un type, le mot-clé self dans une expression se rapporte à un objet de ce type. Sinon, self désigne le type qui possède cette opération.

context Type

stéréotype : expression-ocl

Plusieurs stéréotypes peuvent précéder une expression OCL : - inv : permettant d'exprimer un invariant d'un type donné.

context Type

- Ceci permet de spécifier un invariant d'un type inv : expression-ocl

- pre : permettant de spécifier le comportement d'une opération par une précondition.

context Typename::operationName(param1 : Type1,... ) : ReturnType - Ceci permet de spécifier une précondition d'une opération

pre: expression-ocl

- post : permettant de spécifier le comportement d'une opération par une postcondition.

context Typename::operationName(param1 : Type1,... ) : ReturnType - Ceci permet de spécifier une postcondition d'une opération

post: expression-ocl

Le mot-clé result ne peut figurer que dans une postcondition , où il désigne le résultat de l'évaluation d'une opération.

- body : une expression OCL peut être utilisée pour exprimer le résultat d'une requête.

context Typename::operationName(param1 : Type1,... ) : ReturnType - Ceci permet de spécifier le corps lors de la création d'une opération body: expression-ocl

- init : spécifie la valeur d'un attribut ou d'une association.

context Typename::attributeName(param1 : Type1, ... ) : Type

- - Ceci permet de spécifier la valeur initiale d'un attribut ou d'une association init : expression-ocl

- derive: spécifie les règles de dérivation d'un attribut ou d'une association.

context Typename::assocRoleName(param1 : Type1,... ) : Type

- - Ceci permet de spécifier une dérivation d'un attribut ou d'une association derive: expression-ocl

- def : permet de définir des opérations (ou des variables) qui pourront être (ré)utilisées dans

une expression OCL. Ceci permet de définir des fonctions utilitaires en OCL.

- let : permet de déclarer et de définir la valeur d'un attribut qui pourra être utilisé dans l'ex-

pression qui suit in.

Navigation dans le modèle

En partant d'un objet spécifique, on peut naviguer une association dont le but est de se référer aux objets et leurs propriétés. Pour cela on peut naviguer une association, en utilisant le nom du rôle opposé ou par défaut le nom de la classe opposée en minuscule. object.associationEndName

La valeur de cette expression est un ensemble d'objets de type de la classe de l'association opposée. Cet ensemble dépend de la multiplicité et des qualificatifs associés à l'association.

1.2.4 Exemples

Spécification de la structure de données Pile

La figure 1.1 donne le modèle UML permettant de spécifier la structure de données Pile non générique mémorisant des entiers.

FIGURE 1.1 - Modèle UML de la structure de données Pile

La sémantique de la classe Pile est définie par les contraintes OCL données ci-dessous :

context Pile

inv A1 : vide() implies card()=0
inv A2 : card()=0 implies vide()

Dans le contexte Pile, la notation vide() est équivalente à self.vide().

context Pile ::empiler(x :Integer) post card()= card@pre() +1

post dernier()=x

post not vide()

context Pile ::depiler() pre not vide()

post card()=card@pre()-1

context Pile ::creer() post card()=0

post vide()

context Pile ::dernier() :Integer pre not vide()

L'opérateur @pre donne l'état avant l'exécution. Il est autorisé uniquement au sein d'une post-condition.

Spécification d'une compagnie

La figure 1.2 donne un modèle UML permettant de spécifier une compagnie. Une compagnie est dirigée par une personne. Une personne peut diriger plusieurs compagnies.

FIGURE 1.2 - Modèle UML d'une compagnie

A ce modèle vient s'attacher la contrainte suivante : Le directeur d'une compagnie ne peut pas être considéré comme un employé.

context Compagnie

inv A1 : not(self.dirigée_par.embauchée)

1.3 Mécanisme de typage dans le langage OCL

OCL est un langage typé, voire fortement typé. Chaque expression possède un type qui est explicitement déclaré ou qui peut être dérivé statiquement. L'évaluation de chaque expression OCL doit avoir toujours une valeur dans ce type. La figure 1.3 présente le méta-modèle des types supportés par OCL [10].

FIGURE 1.3 - Le package Types représentant le méta-modèle des types supportés par OCL

Dans la suite, nous expliquons les principales métaclasses qui nous intéressent directement.

TupleType

Le type TupleType permet de regrouper plusieurs champs de divers type à l'instar des types
structurés des langages de programmation commue type struct de C et record de Pascal et d'Ada.

CollectionType

La méta-classe CollectionType modélise la notion d'une collection (Collection) offerte par OCL (voir 1.3.1). Il s'agit d'une méta-classe abstraite ayant quatre descendantes : SetType, OrdredSetType, BagType et SequenceType.

SetType

La méta-classe SetType modélise la notion d'un ensemble (construction Set) offerte par OCL (voir 1.3.1) : pas de doublons et l'ordre n'est pas significatif.

OrdredSetType

La méta-classe OrderdSetType modélise la notion d'un ensemble ordonné (construction OrderdSet) offerte par OCL (voir 1.3.1) : pas de doublons mais l'ordre est significatif.

SequenceType

La méta-classe SequenceType modélise la notion de séquence (construction Sequence) offerte par OCL (voir 1.3.1) : les doublons sont autorisés et l'ordre des éléments est significatif.

BagType

La méta-classe BagType modélise la notion de sur-ensemble (construction Bag) offerte par OCL (voir 1.3.1) : les doublons sont autorisés et l'ordre n'est pas significatif sur les éléments.

1.3.1 Les types collectifs en OCL

Le langage OCL offre des types de base tels que Boolean, Integer, Real, String et enum. Ces types sont dotés de divers opérateurs. En outre, le langage OCL supporte des types collectifs permettant de stocker une collection d'éléments. Ces types collectifs sont modélisés par le diagramme de classes donnée par la figure 1.4.

FIGURE 1.4 - Les types collectifs en OCL

La classe Collection est une classe abstraite et générique. Elle modélise la notion d'une collection d'éléments au sens général. Elle est paramétrée sur le type d'éléments. Elle admet quatre classes descendantes :

- classe Set représente un ensemble mathématique non ordonné ne contenant pas d'éléments dupliqués.

- classe Bag représente un ensemble mathématique non ordonné pouvant contenir d'éléments redondants.

- classe Sequence représente un ensemble mathématique ordonné pouvant contenir d'éléments redondants.

- classe OrdredSet représente un ensemble mathématique ordonné ne contenant pas d'éléments dupliqués.

Opérations de calcul sur les collections

Ces opérations sont :

- select : permet de construire une nouvelle collection à partir d'une collection donnée en sélectionnant des éléments selon un critère donné par un prédicat.

- reject: de manière analogue, construit une nouvelle collection formée des éléments ne vérifiant pas un critère.

- collect : construit une nouvelle collection en évaluant une expression portant sur chaque élément d'une collection donnée. Ceci permet par exemple de réaliser une projection d'une collection par rapport à un attribut de chaque élément.

- forAll : renvoie vrai si un prédicat est vrai pour tous les éléments d'une collection. C'est le quantificateur universel quelque soit ?.

- exists : renvoie vrai si au moins un élément d'une collection vérifie un prédicat. C'est le

quantificateur existentiel il existe ?.

- iterate : permet de balayer les éléments d'une collection d'éléments élément par élément. Sur chaque élément visité, elle effectue une action donnée.

La classe Collection

La classe Collection regroupe plusieurs opérations de consultation (<<query>>). Elles sont au nombre de 10. La sémantique de ces opérations est définie formellement en OCL. Dans la suite, nous donnons les spécifications pré/post des opérations : size, count, includes et excludes. size() : Integer

-Le nombre d'éléments de la collection self

post :result = self ?iterate(elem ;acc :Integer=0|acc+1)

Sachant que elem joue le rôle d'une variable de parcours, acc est l'accumulateur et acc+1 est l'action à effectuer à chaque itération.

count(object : T) : Integer

-Le nombre d'apparitions d'object dans la collection self

post :result = self ?iterate(elem ;acc :Integer=0|

if elem=object then acc+1 else acc endif) includes(object : T) : Boolean

-True sit appartient à self

post :result = self ?count(object)>0 excludes(object : T) : Boolean

-True si object n'appartient pas à self, sinon False

post :result = self ?count(object)=0

Notons au passage, l'utilisation de l'opération count afin de spécifier les deux opérations includes et excludes . Ceci caractérise les spécifications pré/post des types de données abstraits matérialisés par des classes.

La classe Set

La classe Set regroupe plusieurs opérations de consultation (<<query>>). Elles sont au nombre
de 15. La sémantique de ces opérations est définie formellement en OCL. La classe Set est
une classe descendante de la classe Collection. De ce fait, plusieurs opérations sont héritées

de la super classe sans être redéfinies qui sont : size(), includes(), excludes(), includesAll(), excludesAll(), isEmpty(), notEmpty() et sum(). L'opération count() est une opération héritée de la classe ascendante, qui a subi une redéfinition. Les autres opérations, appartenant à la classe Set, constituent l'apport de cette classe. Dans la suite, nous donnons les spécifications pré/post des opérations : count, intersection, including et union.

count(object : T) : Integer

-Le nombre d'apparitions d'object dans la collection self post :result<=1 -pas de redondance dans un ensemble Set

intersection(s :Set(T)) : Set(T)

-permet de calculer l'intersection de self et s

post :result?forAll(elem|self?includes(elem) and s?includes(elem)) post :self?forAll(elem|s?includes(elem)=result?includes(elem)) post :s?forAll(elem|self?includes(elem)=result?includes(elem))

union(s :Set(T)) : Set(T)

-permet de calculer l'union de self et s

post :result?forAll(elem | self?includes(elem) or s?includes(elem)) post :self?forAll(elem | result?includes(elem))

post :s?forAll(elem | result?includes(elem))

including(object :T) : Set(T)

-permet d'inserer un élément object dans self

post :result?forAll(elem|self?includes(elem) or (elem=object)) post :self?forAll(elem|result?includes(elem))

post :result?includes(object)

La classe OrderdSet

La classe Set regroupe plusieurs opérations de consultation ( «query»). Elles sont au nombre de 8. La sémantique de ces opérations est définie formellement en OCL. La classe OrdredSet est une classe descendante de la classe Collection. De ce fait, plusieurs opérations sont héritées de la classe ascendante sans être redéfinies qui sont : size(), includes(), excludes(), count(), includesAll(), excludesAll(), isEmpty(), notEmpty() et sum(). Les autres opérations, appartenant à

la classe OrderdSet, constituent l'apport de cette classe. Dans la suite, nous donnons les spécifications pré/post des opérations : insertAt, first et last.

insertAt(index : Integer, object: T) :OrderdSet(T)

- permet d'insérer un élément object à une postion index dans self post :result?size()=self?size()+1

post :result?at(index)=object

post :Sequence{1..(index-1)}?forAll(i :Integer| self?at(i)=result?at(i))

post :Sequence{(index+1)..self?size()}?forAll(i :Integer| self?at(i)=result?at(i+1))

first() : T

-retourne le premier élément de self
post :result=self?at(1)

last() : T

-retourne le dernier élément de self post :result=self?at(self?size())

La classe Bag

La classe Bag regroupe plusieurs opérations de consultation ( «query»). Elles sont au nombre de 13. La sémantique de ces opérations est définie formellement en OCL. La classe Bag est une classe descendante de la classe Collection. De ce fait, plusieurs opérations sont héritées de la super classe sans être redéfinies qui sont : size(), includes(), excludes(), includesAll(), excludesAll(), isEmpty(), notEmpty() et sum(). L'opération count() est une opération héritée de la classe ascendante, qui a été redéfinie. Les autres opérations, appartenant à la classe Bag, constituent l'apport de cette classe. Dans la suite, nous donnons les spécifications pré/post des opérations: intersection, et including.

intersection(bag :Bag(T)) : Bag(T)

-permet de calculer l'intersection de self et s

post :result?forAll(elem|

result?count(elem)= self?count(elem).min(bag?count(elem)))

post :self?forAll(elem|

result?count(elem)= self?count(elem).min(bag?count(elem)))

post :bag?forAll(elem|

result?count(elem)= self?count(elem).min(bag?count(elem)))

including(object :T) : Bag(T)

-permet d'inserer un élément object dans self

post: result?forAll(elem|

if elem=object then

result?count(elem)=self?count(elem)+1 else

result?count(elem)=self?count(elem) endif)

post: self?forAll(elem|

if elem=object then

result?count(elem)=self?count(elem)+1 else

result?count(elem)=self?count(elem) endif)

La classe Sequence

La classe Sequence regroupe plusieurs opérations de consultation ( «query» ). Elles sont au nombre de 18. La sémantique de ces opérations est définie formellement en OCL. La classe OrdredSet est une classe descendante de la classe Collection. De ce fait, plusieurs opérations sont héritées de la classe ascendante sans être redéfinies qui sont : size(), includes(), excludes(), includesAll(), excludesAll(), isEmpty(), notEmpty() et sum(). L'opération count() est une opération héritée de la classe ascendante, qui a été redéfinie. Les autres opérations, appartenant à la classe Sequence, constituent l'apport de cette classe. Dans la suite, nous donnons les spécifications pré/post des opérations : count, union, insertAt et at.

count(object : T) : Integer

-Le nombre d'apparitions d'object dans la collection self union(s :Sequence(T)) : Sequence(T)

-permet de calculer l'union de self et s

post :result?size()=self?size()+s?size()

post :Sequence{1..self?size()}?forAll(index :Integer| self?at(index)=result?at(index))

post :Sequence{1..s?size()}?forAll(index :Integer|
s?at(index)=result?at(index+self?size()))

insertAt(index : Integer, object: T) :OrderdSet(T)

- permet d'insérer un élément object à une postion index dans self post :result?size()=result?size()+1

post :result?at(index)=object

post :Sequence{1..(index-1)}?forAll(i :Integer|

self?at(i)=result?at(i))

post :Sequence{(index+1)..self?size()}?forAll(i :Integer| self?at(i)=result?at(i+1))

at(i :Integer) : T

-retourne le i-ème élément de self pre :i>=1 and i<=self?size()

1.4 Travaux lies à OCL

Il est utilisé pour décrire la sémantique statique des langages de modélisation comme UML et les profils UML et des langages de méta-modélisation comme MOF. Également, OCL permet d'attacher des propriétés sémantiques aux modèles UML en utilisant avec profit le paradigme conception par contrat (voir 1.1). En outre, OCL peut être utilisé comme langage de requêtes. Enfin, il est de plus en plus utilisé dans le cadre de l'approche MDA préconisée par l'OMG. Dans la suite, nous donnons un aperçu sur les travaux récents liés au langage OCL au sens strict.

Le travail décrit dans [?] préconise l'utilisation de la technique de refactoring afin d'améliorer la compréhension Le langage OCL joue un rôle de plus en plus important aussi bien dans l'activité de modélisation que de méta-modélisation.et la maintenance des spécifications OCL. Les auteurs de ce travail identifient les mauvaises utilisations d'OCL (OCL smells) et proposent une collection de refactorings permettant d'écarter ces OCL smells. Parmi les OCL smells identifiés

(une douzaine) par ces auteurs, nous citons : Implies Chain, Redundancy, Non-atomic rule, And Chain, ForAll Chain, etc.

Le travail décrit dans [?] critique la hiérarchie des types collectifs (voir Figure 1.3) proposée par OCL. Les auteurs de ce travail se démarquent de l'approche orientée opération (spécification pré/post) suivie par l'OMG lors de la définition d'OCL et préconisent une nouvelle approche orientée invariant de classe. Ainsi, ils proposent une nouvelle hiérarchie des types collectifs : Bag et Sequence descendant de Collection et Set et OrderedSet descendent respectivement de Bag et Sequence.

Le travail décrit dans [?] propose une méthode basée sur une approche IDM (Ingénierie Dirigée par les Modèles) permettant de spécifier des opérations de raffinement en utilisant des contrats de transformation exprimés en OCL attachés au niveau méta (M2).

Lors de la manipulation des expressions OCL, deux exceptions peuvent apparaître : invalid et null. La première exception traduit une valeur indéfinie (par exemple division par zéro) et la deuxième traduit une référence nulle à l'instar des langages de programmation orientés objet. Le travail décrit dans [?] propose une formulation des éléments nuls dans le cadre d'OCL basée sur l'environnemnt HOL-OCL [14].

Plusieurs travaux permettent de traduire des contraintes OCL vers des formalismes logiques du premier ordre [?] [?] et d'ordre supérieur [14] [?] existent. De tels traducteurs entraînent la possibilité de raisonner sur des modèles UML équipés des contraintes OCL.

Afin d'ouvrir OCL sur le développement incrémental basé sue la technique de raffinement à l'instar des méthodes formelles comme B [3] et Event-B, nous apportons une extension d'OCL appelée EM-OCL permettant la représentation et la manipulation des objets mathématiques tels que : couple, relation et fonction.

précédent sommaire suivant






Bitcoin is a swarm of cyber hornets serving the goddess of wisdom, feeding on the fire of truth, exponentially growing ever smarter, faster, and stronger behind a wall of encrypted energy








"Il faudrait pour le bonheur des états que les philosophes fussent roi ou que les rois fussent philosophes"   Platon