Techniques avancées d'ingénierie PDF

01/11/2024 Techniques avancées d'ingénierie  Paradigme de la programmation par contrats Contrats de programmation Syntaxe OCL et UML S.ZITI 413 Programmation par contrats Design By Contract (DBC)  Paradigme de programm...

01/11/2024 Techniques avancées d'ingénierie  Paradigme de la programmation par contrats Contrats de programmation Syntaxe OCL et UML S.ZITI 413 Programmation par contrats Design By Contract (DBC)  Paradigme de programmation pour écrire des programmes robustes faciliter la détection des erreurs faciliter la réutilisation du code  Basé sur des pré-conditions, des post-conditions et des invariants. 414 1  01/11/2024 Programmation par contrats Contrat  Relation de confiance entre deux parties client (l’appelant d’un service) fournisseur du service (l’appelé)  Chacune des deux parties s’engage à respecter sa part du contrat. Historique  1980: notation Z (Jean-Raymond Abrial)  Spécification par prédicats 1985: Eiffel (Bertrand Meyer)  Programmation par contrats 2000: Java IContract  2010: Java Cofoja  2012: Ada 415 Programmation par contrats Assertions  Expression booléenne Evaluée à l’exécution (dynamiquement) Vérifier l’état du système  Si le système fonctionne correctement, toutes les assertions doivent être vraies.  Sinon, il y a un bogue.  Trois types d’assertions pour définir des contrats pré-conditions post-conditions invariants 416 2  01/11/2024 Programmation par contrats Pré-conditions  Condition à vérifier par le client avant l’appel d’un service.  Obligation: le client doit satisfaire la pré-condition  Bénéfice: le client est assuré que la post-condition sera satisfaite par le fournisseur Intérêt  Pour le fournisseur établir un contrat d’utilisation dicter les règles à respecter par le client limiter les opérations de vérification et de contre-mesure sur les arguments  Si une pré-condition n’est pas respectée, l’erreur se trouve dans le code du client. 417 Programmation par contrats Post-conditions  Condition à garantir par le fournisseur après l’appel d’un service.  Obligation: le fournisseur doit satisfaire la post-condition  Bénéfice: le fournisseur est assuré que la pré-condition est respectée par le client Intérêt  Pour le client  établir un contrat de résultat  dicter les règles à respecter par le fournisseur  Si une post-condition n’est pas respectée, l’erreur se trouve dans le code du fournisseur. 418 3  01/11/2024 Programmation par contrats Exemple de contrat En pseudo-code double sqrt(double x) requires x >= 0 ensures result >= 0 Math.abs(x - result * result) < 0.001 419 Programmation par contrats Invariants  Condition toujours vraie s’appliquant à une classe ou une interface.  Permet de valider l’état du système.  Bénéfice: vérifier les propriétés d’un objet qui ne devraient jamais changer durant l’exécution 420 4  01/11/2024 Programmation par contrats Évaluation des contrats  Durant l’exécution Pré-condition: avant chaque appel Post-condition: après chaque appel Invariants: avant et après chaque appel  Cas particulier des invariants: En théorie: ne devraient jamais changer En pratique: peuvent changer brièvement entre la pré et la post condition 421 UML et OCL Motivations  Rendre les diagramme UML plus  Ajouter des contraintes à des précis éléments de modélisation  Langage naturel ambigu context Personne inv: self.epouse →notEmpty() implies self.epouse.mari = self and self.mari → notEmpty() implies self.mari.epouse = self } 422 5  01/11/2024 UML et OCL OCL  Langage de description de contraintes de UML.  Permet de restreindre une ou plusieurs valeurs d’un ou de partie d’un modèle.  Utilisé dans les modèles UML ainsi que dans son méta-modèle (à travers les stéréotypes).  Formel, non ambigu, mais facile à utiliser (même par les non mathématiciens). 423 UML et OCL Contrainte OCL  C’est une expression booléenne, sans effet de bord, portant sur les éléments suivants: Types de base: String, Boolean, Integer, Real; Classificateurs et ses propriétés: Attributs, Opération qui sont des "fonctions pures"; Associations; États (des machines d’états associées).  Trois types Invariants de classe: Une contrainte qui doit être respectée par toutes les instances d’une classe. Pré-condition d’une opération qui doit être toujours vraie avant son exécution Post-condition d’une opération qui doit être toujours vraie après son exécution 424 6  01/11/2024 UML et OCL Contrainte OCL  Définition de nouvelles propriétés: Définition de nouveaux attributs ou opérations à l’intérieur d’une classe. Établir la valeur initiale d’un attribut.  Définition de propriétés dérivées: Préciser la valeur d’un attribut ou association dérivés.  Spécifier le corps d’une opération: Spécification d’une opération dans un effet de bord (query). 425 UML et OCL Notation OCL  Directement à l’intérieur d’un modèle ou dans un document séparé: context Personne inv: self.age < 150 context Personne inv: age < 50 Personne +nom: String Personne +age: Integer {age < 150} +nom: String +age:Integer age < 150 426 7  01/11/2024 UML et OCL Notation OCL  Directement à l’intérieur d’un modèle ou dans un document séparé: context Personne inv: self.age < 150 context Personne inv: age < 50 Personne +nom: String Personne +age: Integer {age < 150} +nom: String +age:Integer age < 150 427 UML et OCL Contexte de contrainte  Toute contrainte OCL est liée à un contexte spécifique, l’élément auquel la contrainte est attachée.  Le contexte peut être utilisé à l’intérieur d’une expression grâce au mot-clef «self». Implicite dans toute expression OCL. Similaire de «self» dans Smalltalk ou Python Similaire de «this» de C++ et Java, ou au Similaire de «Current» dans Eiffel 428 8  01/11/2024 UML et OCL Expression OCL de l’invariant d’une classe  Dans un état stable, toute instance d’une classe doit vérifier les invariants de cette classe.  Expression OCL stéréotypée «invariant»: Context e : Etudiant inv ageMinimum: e.age > 16 Context e : Etudiant inv : e. age > 16 Context Etudiant inv : self. age > 16 429 UML et OCL Eléments de base d’une expression OCL  Les éléments suivants peuvent être utilisés dans une expression OCL: Les types de base: String, Boolean, Integer, Real. Les Classificateurs et leurs propriétés: Attributs d’instance et de classe. Opérations de Query (i.e. sans effet de bord) d’instance et de classe. États des machines d’états associées. Associations du modèle UML. 430 9  01/11/2024 UML et OCL Types de base et opération Type Values Opérations Boolean true, false And, or, xor, neg,... Integer 1, -5, 2, 34, 26524,... =, *, +, -, /, abs, div, mod, max, min, >, , 10 433 UML et OCL Propriétés  Opération de Query: Notation pointée: Opérations d’instance: context Etudiant self. age()> 16 Opérations de classe: context Etudiant inv : self. age() >Etudiant.ageMin()  Etat: Accessible avec oclInState(): context Departement:: ajouter (e: Enseignant) pre: e. oclInState ( disponible ) pre: e. oclInState ( indisponible :: en vacances) −− etats imbriques 434 11  01/11/2024 UML et OCL Spécification d’opération  Inspirée des Types Abstraits: une opération est composée par une signature, des pré- conditions et des post-conditions.  Permet de contraindre l’ensemble de valeurs d’entrée d’une opération.  Permet de spécifier la sémantique d’une opération càd sa fonctionnalité  Pré-condition: context Departement:: ajouter (e:Enseignant):Integer pre nonNul: e. notNil ()  Poste-condition: avec les opérateurs spéciaux @pre la valeur d’une propriété d’avant l’opération et result le résultat de l’opération Context Etudiant :: age() :Integer post correct : result= (today− naissance ). years () Context Typename::operationName(param1: type1, param2: type2,…) Type post resultOk :result=... 435 Contrats en Eiffel/Java Contrats et langages de programmation Conception par contrats en Eiffel/Java Vérification des contrats S.ZITI 436 12  01/11/2024 Contrats et langages de programmation Lien entre contrats et langages de programmation Les contrats sont vérifiés dynamiquement comment écrire les contrats? ○ dans le langage de programmation? ○ à côté? comment vérifier les contrats? ○ quand? ○ quel outil? 437 Contrats et langages de programmation Contrats et langages de programmation Plusieurs façon d’intégrer la programmation par contrats à un langage nativement (directement dans le langage) ○ Eiffel, D, Lisaac, Spark, VDM, Ada via des pré-processeurs et des commentaires ou annotations spécifiques ○ Java IContract, Java Cofoja via des macros ○ C, C++ 438 13  01/11/2024 Contrats et langages de programmation Contrats en Eiffel Depuis 1987 Support natif des contrats Constructions pour les méthodes ○ bloc require(pré-condition) ○ bloc ensure(post-condition) Construction pour les classes/interfaces ○ bloc invariant https://www.eiffel.com/values/design-by-contract/introduction/ 439 Contrats et langages de programmation Exemple de contrat en Eiffel class DICTIONNAIRE[G] feature ajouter(x: G; cle: STRING) is require taille < capacite not cle.empty do -- code d’insertion ensure has (x) item (cle) = x taille = old taille+1 -- reste du code end 440 14  01/11/2024 Contrats et langages de programmation Contrats en Java Nous avons déjà vu les assertions. Deux approches via des pré-processeurs 2000: Java IContract basé sur des commentaires déprécié depuis quelques années... 2010: Java Cofoja basé sur des annotations Java supporté par Google 441 Contrats et langages de programmation Exemple avec les assertions double sqrt(double x) { assert x >= 0.0 // … définir la valeur de retour `res` assert res >= 0.0 assert Math.abs((res * res) - x) < 0.001 } 442 15  01/11/2024 Contrats et langages de programmation Exemple avec Java iContract double sqrt(double x) { //... } http://www.javaworld.com/article/2074956/learn-j ava/icontract-- design-by-contract-in-java.html 443 Contrats et langages de programmation Exemple avec Java Cofoja @Requires("x >= 0.0") @Ensures({ "result >= 0.0", "Math.abs(result * result - x) < 0.001" }) double sqrt(double x) { return Math.sqrt(x); } https://github.com/nhatminhle/cofoja 444 16  01/11/2024 Contrats et langages de programmation Contrats en C/C++ Deux approches pour le langage C 1995: APP basé sur des commentaires et un pré-processeur Macros basé sur des macros de compilation 445 Contrats et langages de programmation Exemple C avec APP float sqrt(float x) { //... } D. S. Rosenblum. A practical approach to programming with assertions. IEEE Trans. Soft. Eng., 21(1):19-31, 1995. 446 17  01/11/2024 Contrats et langages de programmation Exemple C avec macro Fichier assert.h void assert( int expression ); Définition de la macro: #ifdef NDEBUG #define assert(expr) 0 #else #define assert(expr) \ (expr) ? 0 : assert_fail( STRING(expr), FILE , LINE ) #endif 447 Contrats et langages de programmation Exemple macro C Utilisation de la macro #include int sqrt(int x) { assert(x >=0) // … } 448 18  01/11/2024 Contrats et langages de programmation Contract For Java (Cofoja) Contrats pour Java https://github.com/nhatminhle/cofoja Nhat Minh Lê (Google) dernière version: février 2016 Java 1.6 à 1.8 open-source 449 Contrats et langages de programmation Exemple import com.google.java.contract.Ensures; import com.google.java.contract.Requires; public class Main { @Requires("x>=0.0") @Ensures({ "result >= 0.0", "Math.abs(result * result - x) < 0.001" }) public static double sqrt(double x) { return Math.sqrt(x); } public static void main(String[] args) { // pre-condition OK double x = sqrt(100); System.out.println("x = " + x); // pre-condition FAIL x = sqrt(-100); System.out.println("x = " + x); } } 450 19  01/11/2024 Contrats et langages de programmation Fonctionnement javac java.java.class processeur contract tisseur d’annotations contrats 451 Contrats et langages de programmation Utiliser Cofoja Nécessite un jar pour fonctionner cofoja.contracts.asm-VERSION.jar version stable actuelle 1.3 Télécharger les dépendances sur https://github.com/nhatminhle/cofoja/releases 452 20  01/11/2024 Contrats et langages de programmation Cofoja en ligne de commandes Compiler avec les annotations: javac \ -d bin/ -cp cofoja.jar \ -processorpath cofoja.jar \ src/Main.java Exécuter avec les contrats: java -cp bin/ -javaagent:cofoja.jar Main 453 Contrats et langages de programmation Conclusion Programmation par contrats basés sur les pré / post-conditions et invariants facilitent la conception modulaire définissent les attentes et responsabilités du client et du fournisseur permettent un code plus robuste, sûr 454 21