Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

COO : Spécification du logiciel - OCL Philippe Collet Licence 3 – parcours Info

COO : Spécification du logiciel - OCL Philippe Collet Licence 3 – parcours Informatique et MIAGE Septembre - Décembre 2012 © Ph. Collet 2 Objectifs r Comprendre l’activité de spécification logicielle r Apprendre la spécification par assertions r Comprendre la nécessité et la portée d’OCL r Apprendre OCL et la manière de spécifier avec ce langage dans UML r Comprendre les techniques de vérification des assertions © Ph. Collet 3 Plan r Introduction aux spécifications r Introduction à la spécification par assertions r OCL : première approche r Types et valeurs de base r Navigation dans les modèles r Autres éléments du langage r Collections r Conception par contrats r Annexe OCL © Ph. Collet 4 Introduction aux spécifications r Spécification fonctionnelle : définition r Principaux formalismes de spécification r Notions autour de la spécification r Spécification en langage naturel r Tour rapide d’autres techniques de spécifications « formelles » © Ph. Collet 5 Spécification fonctionnelle r Définition : n définir ce que doit faire un logiciel ... n avant d’écrire ce logiciel ! n => le quoi, sans le comment ! r S’oppose à implémentation, n comme le plan d’un pont à sa construction. n Sauf... qu’en informatique, plan et réalisation ne manipulent que de l’écriture... © Ph. Collet 6 Pourquoi spécifier ? r Définir le travail de réalisation, avant de le faire ... n la spécification est censée être moins coûteuse, plus rapide à obtenir r Comment vérifier la correction d’un programme, n si l’on ne sait pas ce qu’il est censé faire ... n la spécification est la référence pour toutes les activités de vérification et de validation (V&V) : u tests, preuves, mesures, inspections... r Obtenir une description stable, plus abstraite, moins dépendante des contingences du matériel, des systèmes, des fluctuations de l’environnement. © Ph. Collet 7 Qualités recherchées pour une spécification fonctionnelle r précision, non ambiguïté, non contradiction, r concision, abstraction, r complétude, r facilité d’utilisation : écriture, lecture, vérification r réalisable avant l’implémentation, r si possible à un coût réduit, r référence contractualisable, pour les litiges... © Ph. Collet 8 Spécifications fonctionnelles vs extrafonctionnelles r En génie logiciel, on distingue : n spécification fonctionnelle : décrit le « fonctionnement » du logiciel, le quoi n spécification extrafonctionnelle (ou non fonctionnelle) : les conditions de fonctionnement, le comment r Dans le monde industriel, spécification sous-entend, spécifications techniques r En génie logiciel, par défaut spécification sous-entend spécification fonctionnelle r Les spécifications techniques du logiciel : coût, temps de réponse, performance, robustesse, capacité de charge, consommation de ressource, confort d’utilisation, ergonomie ... sont appelées : n qualités de service (QoS) n spécifications non fonctionnelles n spécifications extrafonctionnelles © Ph. Collet 9 Principaux formalismes de spécification r Texte informel n En langage naturel (cahier des charges, commentaires) n éventuellement encadré par une méthode ou un formalisme graphique (contraintes UML) r Graphique n sauf exception (réseaux de Petri...) rarement très formel : (SADT, UML) n pas très précis, mais utile pour la synthèse et en complément r Semi-formel n Sans ambiguïté, leur expressivité est insuffisante pour établir une preuve, mais on peut souvent les tester : u techniques assertionnelles, spécification axiomatique r Formel n Sans ambiguïté, leur expressivité est suffisante pour tout décrire, donc pour établir des preuves, humaines (« à la main ») ou automatiques © Ph. Collet 10 Spécification vs Implémentation r Spécification n décrit ce que doit faire le logiciel, si possible très tôt dans le processus logiciel, à un coût faible, indépendamment des « détails » : u type de machine, plate-forme, langage utilisé, conditions d’utilisation, fréquences des primitives, représentation, formats... n Une spécification fonctionnelle doit se concentrer sur les fonctionnalités, sans considération de performance ou de qualités de services (spécifications extrafonctionnelles) r Implémentation n doit correspondre aux fonctionnalités décrites (idée de correction), n mais de manière efficace, performante, en tenant compte: u des conditions réelles ou prévues d’utilisation : langage, spécificité du langage utilisé, fréquence d’emploi des primitives fournies, volumes des données traitées... n des contraintes exprimées dans les spécifications extrafonctionnelles © Ph. Collet 11 Spécification vs Implémentation (suite) r En simplifiant, r spécifier, c’est définir n sans se soucier des contingences du monde réel... r implémenter, c’est optimiser, réifier n c’est tenir compte de la réalité... r Si l’implémentation nécessite beaucoup de détails, l’écart de niveaux d’abstraction avec la spécification est grand, et cela nécessite des descriptions intermédiaires : n approches par raffinements successifs © Ph. Collet 12 Spécification vs Implémentation (suite) r Relations d’abstraction et de raffinement n Considérons une suite de n descriptions du même problème, à différents niveaux d’abstraction, numérotées par niveau d’abstraction décroissant : u desc1 ⊆ desc2... ⊆ descn n la desc1, de plus haut niveau d’abstraction, u est la spécification, n la descn, de plus bas niveau d’abstraction, u est l’implémentation r Toutes les descriptions sont liées par deux relations : n abstraction : u desci = abstract(desci+1) ⇔ desci ⊆ desci+1 n raffinement : u desci = refine(desci−1) ⇔ desci ⊇ desci−1 r Il existe une théorie qui formalise ces relations : refinement calculus © Ph. Collet 13 Spécification, Formalité et Exécutabilité r Deux sens au mot formel : 1. formel = non ambigu, précis, sans équivoque u syntaxe et sémantique précise, interprétable par une machine 2. formel = privilégie la forme au détriment du contenu u non ambigu et vérifiable, prouvable à la main ou automatiquement. r Exemple: (a + b)² = a² + 2ab + b² r formel n’implique donc pas abstrait (sens 1), mais on confond souvent les deux mots (sens 2) r Exemple : n logique formelle, avec des formules, par opposition à logique philosophique, avec (beaucoup) de mots... (sens 2) n spécification (formelle) et implémentation sont formelles ! (sens 1) u ... puisque sans ambiguïté !!! © Ph. Collet 14 Spécification, Formalité et Exécutabilité (suite) r Mais n un programme dans un langage de bas niveau se prête difficilement à des preuves, c’est-à-dire à l’établissement de propositions vraies pour toutes exécutions : n généralement, on teste un programme exécutable r Inversement, n une preuve théorique de spécification ne prouve pas que le logiciel décrit sera utilisable : n temps de réponse ? ergonomie ? adéquation aux besoins ? r La frontière entre spécification et implémentation est assez floue et arbitraire et dépend des époques : n il y a quelques années, un texte en Prolog aurait été considéré comme une spécification abstraite exécutable… © Ph. Collet 15 Spécification fonctionnelle et correction r Qualité de correction n un logiciel est correct, si dans des conditions normales d’utilisation, il se comporte comme cela est attendu par ses utilisateurs n Si la spécification traduit bien ce que veulent les utilisateurs, alors la correction revient à vérifier (prouver, tester) que l’implémentation est conforme à sa spécification r Conséquences : n Pour vérifier la correction d’une description, il faut une deuxième description : la redondance est indispensable à tout contrôle : preuve par neuf, contrôle de qualité, vérification des cartes perforées (autrefois)... n Comment vérifier la correction d’une spécification ? u l’un des gros problèmes des spécifications formelles, lorsqu’elles sont incompréhensibles aux commanditaires ou aux utilisateurs © Ph. Collet 16 Utilisation des spécifications fonctionnelles r définition du travail d’implémentation, n à un coût normalement inférieur : l’équivalent des plans d’un immeuble, d’une machine, avant sa réalisation. n (sauf qu’ici, spécification et implémentation, c’est de l’écriture !) r référence pour tout ce qui concerne les fonctionnalités du logiciel : n les documentations d’utilisation, de maintenance, les tests externes, les preuves de correction... © Ph. Collet 17 Spécification en langage naturel r Description en langage naturel (anglais, français...) : n de manière complètement libre, littéraire... n de manière très encadrée (structurée) par une méthode qui fournit un plan précis de ce qu’il faut décrire n Exemples : normes de cahiers des charges (ISO 900x, IEEE 930), outils d’aide à la documentation pour certains langages de programmation (Java, Eiffel) ou certains systèmes (Unix, Emacs...) r Utilisation d’une syntaxe pour les aspects structurels, les signatures de méthodes... n importance de la phase de conception préalable r Utilisation de glossaires ou de dictionnaires de données (identificateurs...) n pour éviter d’utiliser des mots voisins ou synonymes : utiliser au contraire un seul mot pour chaque concept r Règles de description et d’abréviations n Exemple : un prédicat rend une valeur logique vraie ou faux, donc il suffit de décrire le cas vrai © Ph. Collet 18 Exemple d’une (mauvaise) spécification en langage naturel r Ce module gère une file d’attente de transactions selon l’ordre premier arrivé - premier servi (FIFO)... r La queue a au plus 500 transactions et est manipulée par les opérations suivantes : n déposer une transaction dans la file, à la fin, si c’est possible, sinon envoyer le message d’erreur “déposer impossible”. n retirer la première transaction de la file (la plus ancienne, en tête), si elle existe, sinon donner le message d’erreur “retirer impossible”. n connaître à tout instant la longueur de la file. © Ph. Collet 19 Avantages de la spécification en langage naturel r (en uploads/Ingenierie_Lourd/ l3-specocl-201213.pdf