Introduction

Quelques rappels

• module - un ensemble de programmes envisagé pour affectation cohésive de travail
• les choses qui peuvent changer devraient être privées.
• les interfaces devraient faire abstraction de "secrets".

Qu’est-ce que des spécifications ?

1. Définition générale de spécifications
   • Information spécifique sur l’objet
2. Définition du point de vue du génie logiciel
   • information spécifique sur les exigences que l’objet doit rencontrer.
   • descriptions sous forme de "boîtes noires"
   • décisions concernant le design ne sont pas des exigences
   • propriétés comme "facilité de changement" sont des exigences
3. Nous allons utiliser ce terme au sens B.

Pourquoi avons-nous besoin de spécifications de modules ?

• Projets ayant plusieurs réalisateurs
• Projets ayant plusieurs versions
• "Notre incapacité de faire beaucoup" (E.W.Dijkstra)
• Chaque tâche devrait avoir une définition indépendante du reste du travail.
• Nous prenons des décisions explicites et précises au début
  • suppositions intra-modulaires
  • report de décisions à plus tard

Spécification formelle

Une spécification est formelle si elle est écrite dans un langage dont la syntaxe et la sémantique sont définies précisément.

• Pas nécessairement des caractères grecs, exposants, indices
• Basée sur des formes restreintes et des règles d’interprétation strictes
  • Chances de fausse interprétation réduites
  • Interprétable mécaniquement
• Pas "superficielle"

Exemples de langages de spécification : langage de mathématiques, Java, ML, ...

Pourquoi pas une langue naturelle (français, anglais, chinois, allemand, ...?)

• Interprétation exige un système légal élaboré
• Exemples d'ambiguïtés dans une spécification écrite dans une langue naturelle :
  1. "Retourne le sommet de la pile"
  2. "Enlève l’élément qui se trouve au sommet de la pile"
  3. "Le domaine de la fonction d'abstraction est formé de toutes les valeurs possibles de la fonction"
  4. "Si on introduit un nombre supérieur à la représentation interne, on déclenchera l’exception X"

Pourquoi des spécifications doivent-elles être précises ?

• Décisions prises au début, de façon dispersée, sont difficiles à corriger
• Empêcher l’incompatibilité entre les composantes
• Permettre d’éviter une distribution excessive de l’information
• Minimiser des suppositions restreignantes

Spécification abstraite

Une spécification est abstraite si elle est écrite entièrement en terme du comportement observable du module.

Pourquoi des spécifications doivent-elles être abstraites ?

• Abstraction - un modèle, plusieurs réalisations
• Il faut admettre plusieurs versions
• Exprimer seulement les exigences (exemple: tri fictif)
• Moins d’information à comprendre
• L’usager est concerné seulement par les faits qu’il peut découvrir lui-même par l’usage légitime

Classes de spécification

Quatre classes des techniques de spécification de logiciel :

1. spécifications basées sur le concept de modèle abstrait
2. spécifications algébriques
3. spécifications basées sur le concept de trace
4. spécifications basées sur le concept de processus

Pour les classes 1. et 4. des modèles doivent être construits pour représenter des particularités importantes d’objets abstraits.

Les classes 2. et 3. sont des techniques de "boîte noire".

Spécifications basées sur le concept de modèle abstrait

• VDM, Z, Object-Z
• le modèle d’un module est construit à partir des structures de données et opérations dont le sens est bien compris
• le comportement exigé du module est décrit en montrant comment le modèle se comporte

Spécifications algébriques

• Larch, CLU, OBJ, Affirm
• valeurs d’objets abstraits et opérations forment une algèbre
• les axiomes expriment les propriétés de l’algèbre

Spécifications basées sur le concept de trace

• approche "automate à états finis"
• histoire d’un objet
• traces canoniques

Spécifications basées sur le concept de processus

• LOTOS, Estelle, CSP
• utilisées pour processus simultanés et répartis
• modélisées par processus parallèles

Exemples

Définition du type File d'entiers en LOTOS :

type int_file is integer with
  sorts file
  opns  _:   → file
    ADD: integer, file → file
    FRONT: file → integer
    REMOVE: file → file
  eqns forall x,y: integer, q: file
    ofsort integer
    FRONT(_) = 0;
    FRONT(ADD(x,_)) = x;
    FRONT(ADD(x,ADD(y,q))) = FRONT(ADD(y,q));
    REMOVE(_) = _;
    REMOVE(ADD(x,_)) = _
    REMOVE(ADD(x,ADD(y,q))) = ADD(x,REMOVE(ADD(y,q)));
endtype

défauts :

• problèmes avec situations inattendues
• comment limiter le nombre d’éléments dans une file ?
• comment traiter le non-déterminisme ?

Définition du type Agenda d’anniversaires en Z

______Agenda______
connus: ℘(NOM)                          // l'espace d'états
anniversaire: NOM → DATE                // (déclarations des variables)
__________________
connus = dom anniversaire               // L'invariant du système (relations
                                        // entre les variables)

______AjouterAnniversaire______
ΔAgenda                                 // schéma d'opération (4 variables : connus,
                                        // connus', anniversaire, anniversaire')
nom? : NOM                              // argument d'entrée
date? : DATE                            // argument d'entrée
__________________
nom? ∉ connus
anniversaire' = anniversaire ∪ {nom? → date?}

Exercice: Montrer que: connus’ = connus ∪ { nom? }

______TrouverAnniversaire______
ΞAgenda                                 // schéma d'interrogation
nom? : NOM                              // argument d'entrée
date! : DATE                            // argument de sortie
__________________
nom? ∈ connus
date! = anniversaire(nom?)

______Rappeler______
ΞAgenda
aujourd'hui? : DATE
cartes! : ℘(NOM)
cartes! = { n: connus | anniversaire(n) = aujourd'hui? }

______InitialiserAgenda______
Agenda                                  // schéma d'initialisation
__________________
connus = ∅

Spécifications de modules versus spécifications de programmes

• Programmes ne cachent pas de données.
• Effets de programmes peuvent être décrits en fonction de structures de données.
• Effets de programme sont visibles instantanément.
• Modules ont des données cachées.
• Spécifications de modules peuvent ne pas mentionner la structure de données.
• La visibilité des effets de module peut être retardée.

Nous utilisons des spécifications relationnelles pour des programmes.

Nous utilisons des assertions sur les traces pour des modules.

Les deux sont complètement compatibles.