- LORIA Nancy, France Institut de la Francophonie pour l'Informatique. - de la spécication à l'implantation. - Mes plus sincères remerciements vont également à tous les professeurs et les personnels de l'Institut de la Francophonie pour l'Informatique (IFI) pour m'avoir donnée des cours de très grande qualité et pour leur soutien tout au long de mes études à l'IFI.. - Je remercie chaleureusement mes camarades de la promotion XII pour leur amitié sans faille et je leur souhaite bonne chance pour la soutenance.. - Nous avons proposé une liaison à diérents niveaux : celui de la programmation avec la dé- nition d'adaptateurs à partir des EJBs existants . - celui de la spécication avec la dénition de la compatibilité entre méthodes à l'aide de Java Modeling Language (JML).. - 3.2 Résumé la compatibilité entre deux méthodes avec exception(s. - Notre travail consiste à étudier la compatibilité entre méthodes de l'interface requise et celles de l'interface fournie en utilisant JML.. - de l'Information et de la Communication, la formation par la recherche en partenariat avec les Universités lorraines et le transfert technologique par le biais de partenariats industriels et par l'aide à la création d'entreprises.. - L'objectif de cette équipe est d'étudier les mécanismes de construction de spécications et de programmes, dans le but d'acquérir une meilleure maîtrise de la production, de l'évolution et de la qualité des logiciels. - La mémoire est structuré de la manière suivante.. - Nous présentons aussi des travaux concernant la compatibilité de signa- tures et de spécications qui jouent un rôle important dans la compatibilité entre interfaces.. - l'interface requise. - La méthode B [1] est une méthode qui supporte la spécication formelle des interfaces et permet aussi la preuve de leur interopérabilité [4, 15].. - Les autres clauses du modèle générique de la gure 2.1 ont trait à la modularité : seen_model de la clause SEES est un modèle B qui peut être vu mais dont l'état ne peut pas être modié.. - included_model de la clause INCLUDES est un autre modèle B dont l'état est visible et dont les changements peuvent être contrôlés en appelant ses opérations.. - En d'autres termes, nous pouvons dénir l'interopérabilité entre composants de la manière suivante à l'aide de B [4].. - Durent peu de temps - Durent peu de temps - Durent longtemps (leur durée de vie est la même que celle des données de la base de données. - Si l'état d'une entité est modié par une tran- saction lors de la destruction du conteneur, l'état de l'entité est reconstitué à partir de l'état de la dernière transaction eectuée - Sont appelés de manière asyn-. - Nous présentons dans le gure 2.6 un exemple générique d'application client/serveur complet en utilisant des EJBs.. - Les composants B et C (gure 2.8) sont déclarés en utilisant des annotations d'EJB.. - Le composant C est déni de la même manière que B. - Spécication de types C'est la partie statique du modèle, elle contient des propriétés qui portent sur les attributs de la classe [17]. - ce sont les propriétés portant sur les attributs de la classe qui doivent être vraies dans tous les états "visibles". - condition qui doit être remplie par le système et les paramètres de la méthode pour que la méthode puisse être exécutée Divergence (clause diverges predicat J M L. - liste des attributs qui sont modiés par l'exécution de la méthode. - Le predicat J M L indique la postcondition qui doit être vériée à la n de la méthode quand celle-ci se termine en levant une exception exp de type Exception1.. - La forme générale d'un comportement est dénie dans le gure 2.10.. - public : visible depuis n'importe quelle autre classe private : visible uniquement à l'intérieur de la classe. - Cela veut dire que dans JML, la condition de la clause signals est false. - En d'autres termes, la condition de la clause ensures est false. - Dans l'interface PI_MLights, les deux variables color et ml_state sont déclarées au niveau spécication de la manière suivante. - en relation avec notre approche, en vue de les appliquer pour dénir la compatibilité entre méthodes spéciées en JML.. - La compatibilité de spécications est un processus pour déterminer si deux composants sont comparables et vise à répondre aux questions suivantes. - La compatibilité entre ces deux composants C et C' est dénie par. - La compatibilité de signatures de méthodes utilise la compatibilité de types. - Généralement, en supposant que nous avons le type des méthodes dans la bibliothèque de composants, τ l , et le type de la requête, τ q , alors la compatibilité M( τ l , τ q ) est dénie par. - ∃T l and T q such that T l (τ l ) R T q (τ q ) (2.2) Dans lequel. - T l et T q sont des transformations appliquées pour le type de la bibliothèque et celui de la requête. - La compatibilité de signatures est fonction de la relation R entre τ l et τ q et des transfor- mations T l , T q. - Compatibilité exacte A partir de la formule 2.2, si : τ l est une suite de renommages des variable V, τ q est la fonction identité,. - La compatibilité est dite exacte. - τ l ≤ τ q (2.4) Intuitivement, un type disponible en bibliothèque est compatible avec celui de la requête si le type de la requête est plus général que celui de bibliothèque.. - S R b 2 Q post ) (2.5) Avec. - A partir de la formule 2.5, avec S b = S post et R 1 et R 2 sont une équivalence, nous obtenons la formule de Compatibilité pré/post exacte suivante. - Donc, addR pre ⇔ addP pre et addP post ⇔ addR post , correspondant à la compatibilité exacte.. - Compatibilité plug-in L'idée de compatibilité plug-in est exprimée gure 2.12.. - une méthode S <. - À partir de la formule 2.5, avec S b = S post . - (S post ⇒ Q post ) (2.8) La compatibilité plug-in est illustrée par l'exemple suivant. - la compatibilité entre addR et addP est donc plug-in.. - Compatibilité exacte À partir de formule 2.6, la compatibilité exacte correspond au cas où R est une équivalence. - Les trois cas de la gure 3.1 sont fondés sur l'utilisation d'un (ou deux) composant(s) existant(s) OTS (OTS1 et OTS2. - Dans le cas général présenté gure 3.4, le composant DEV est déni par l'assemblage de plusieurs composants. - 3.11 Étude de cas exprimée dans EJB La spécication est réalisé en EJB de la manière suivante. - Les interfaces RI_Lights et PI_Lights sont présentées dans la gure 3.12.. - Pour résoudre ce problème, nous ajoutons des méthodes get/set pour chaque variables déclarons dans l'inter- face : une pour obtenir la valeur de la variable et une autre pour modier cette variable qui est déclarée dans la classe qui implante cette interface. - Comme présenté dans la section 2.4.2, la compatibilité de signatures de méthodes est basée sur la compatibilité de types. - La vérication de la compatibilité de signatures peut être eectuée par le compilateur Java. - Examinons la compatibilité de signatures entre les méthodes payInterest(double rate) des interfaces BankAccount et Account (voir gure 3.14).. - Soit τ q le type de la méthode payInterest(double rate) d'interface BankAccount, τ l est celui d'interface Account. - Ceci correspond à la compatibilité exacte dénie par A.. - comme présenté gure 3.14. - Nous avons. - Sachons que Money est une super-interface de MoneyOps (voir gure 3.15), nous pouvons remplacer MoneyOps par Money selon la règle du renommage des variables [30], alors τ q = V τ l , correspondant à la compatibilité de signatures exacte.. - Donc, τ q = V τ l , correspondant à la compatibilité exacte.. - Wing sur la compatibilité entre méthodes. - Illustrons la compatibilité dans ce cas par l'exemple suivant. - Pour l'interface CounterR, il existe un invariant mais il n'y a pas de précondition de la méthode incR. - Après combinaison avec l'invariant, la précondition et la postcondition de la méthode incR sont exprimées comme suit. - Pour l'interface CounterP, il n'y a pas d'invariant, la précondition et la postcondition de la méthode incP sont inchangées. - Pour une méthode impure, dans le comportement, nous déclarons une liste des variables modiées à l'aide de la clause. - La compatibilité entre ces deux méthodes est donc vériée à l'aide de leur comportement.. - result) Selon la dénition de la compatibilité entre deux méthodes. - Cela correspond à la compatibilité plug-in entre les deux méthodes addR et addP. - Il faut ajouter que nous considérons seulement la compatibilité entre les deux méthodes. - Si nous vérions la compatibilité entre les deux interfaces, ce n'est pas vrai ça ne marche pas parce que addP modie la variable globale somme.. - Si la visibilité de la variable est private, cela signie que la variable est utilisée seulement dans son interface, elle n'est pas utilisée à l'extérieur. - Si la visibilité de la variable est protected ou public, lorsqu'une méthode d'interface requise utilise une variable de l'interface fournie de ce type, ces deux types de visibilité sont utilisables.. - Une question se pose alors : comment déterminer la compatibilité entre deux méthodes ayant plusieurs comporte- ments. - Cas 1 C'est le cas le plus simple, nous comparons la précondition et la postcondition cor- respondante de la méthode de l'interface requise et celle de l'interface fournie en utilisant soit la compatibilité pré/post soit la compatibilité de prédicats.. - Cas 2 Utilisation de la compatibilité pré/post condition.. - Pour l'exemple précédent, la compabilité est véri- ée de la manière suivante. - Cette formule prouve aussi que le deuxième exemple ne satisfait pas la compatibilité.. - En général, la compatibilité entre deux méthodes, l'une avec un comportement et l'autre avec n comportements, est dénie par. - Elles peuvent également être spéciées au niveau de la spécication JML. - La compatibilité entre deux méthodes est exprimée par : if((R pre ⇒ P pre ) 4 and (R pre. - La notion d'exception n'est donc pas concernée avec la compatibilité entre les deux mé- thodes dans ce cas.. - Si subR pre = true , alors subP pre = true et nous vérions la relation entre subP post et subR post pour déterminer la compatibilité.. - À l'aide des deux cas précédents, la compatibilité entre deux méthodes est basée sur des comportements normaux, pas de comportements exceptionnels, illustré par l'exemple suivant. - La compatibilité entre les deux méthodes est exprimée de la manière suivante : if. - 3.2 Résumé la compatibilité entre deux méthodes avec exception(s). - En conclusion, la compatibilité entre deux méthodes dans lesquelles il existe une (plusieurs) exception(s) est exprimée par. - La compatibilité entre deux méthodes sans exception(s). - Wing sur la compatibilité de spécications, une dénition de la compatibilité directe entre deux méthodes déclarées dans leur interface en Java et dont le comportement est spécié en Java Modeling Language.. - et par la compatibilité entre méthodes à l'aide de JML.. - Il est aussi envisageable de formaliser le lien entre UML/B et EJB à l'aide des travaux existants autour de la traduction automatique B vers Java [29, 25].. - En se basant sur la compatibilité de méthodes, notre approche peut être améliorée par l'étude de la compatibilité entre deux interfaces. - La compatibilité entre deux méthodes correspondantes de l'interface requise et de l'in- terface fournie. - Dans le cas de la compatibilité directe entre deux interfaces, l'adapateur entre interface requise et interface fournie correspond à l'adaptateur "nul", nommé Γ 0