Spécification (informatique)

Un article de Wikipédia, l'encyclopédie libre.

Vous avez de nouveaux messages (diff^?).

Cet article est une ébauche à compléter concernant l'informatique, vous pouvez partager vos connaissances en le modifiant.

En génie logiciel il s'agit d'une étape du développement d'un programme ou d'un système informatique qui consiste à décrire ce que le logiciel doit faire puis comment il doit le faire.

Sommaire

1 Types de spécification
2 Méthode de spécification
3 Exemples
- 3.1 L'Analyse fonctionnelle descendante (SADT)
- 3.2 La Méthode B
4 Validation de spécification
5 Formel vs rigoureux
6 L'écriture des commentaires d'une spécification formelle
7 Voir aussi
- 7.1 Liens externes
  - 7.1.1 Prouveurs
  - 7.1.2 Model chekers

[modifier] Types de spécification

On distingue :

les spécifications informelles
les spécifications semi-formelles
les spécifications formelles

On distingue également (notamment dans la méthode Merise) :

les spécifications générales ou externes (spécifications fonctionnelles générales ou SFG)
les spécifications détaillées ou internes (spécifications fonctionnelles détaillées ou SFD)
les spécifications techniques.

On distingue aussi les spécifications par le ou les paradigmes utilisées (par exemple, des processus séquentiels communicants (CCS, CSP), ensembliste, etc.). Ainsi on peut spécifier sans utiliser de variables (comme en « pur » CCS).

On parle de « spécifications mixtes » quand on utilise plusieurs paradigmes. Par exemple, une méthode semi-formelle comme JSD (auteurs : M. Jackson, J. Cameron), utilise le paradigme des processus séquentiels communicants mais avec « passage de valeur » (avec variables).

On trouve aussi la classification suivante :

spécifications exécutables
spécifications non exécutables.

Selon la définition que l'on donnera à ce qu'est une spécification, on pourra considérer qu'une spécification ne doit pas être exécutable (c'est ce qui la distingue, entre autres choses, d'un programme).

[modifier] Méthode de spécification

Le terme « méthode de spécification » recouvre :

une méthode (ordre des tâches préconisé pour réaliser une spécification)
un langage pour écrire la spécification. Ce langage peut être informel ou formel. Dans ce dernier cas, on distingue :
- les langages avec une syntaxe formelle
- les langages avec une syntaxe et une sémantique formelles
- des outils d'aide :
  - éditeurs
  - vérificateurs de syntaxe
  - vérificateurs de typage
  - prouveurs (en général, la logique sous-jacente au langage de spécification n'est pas décidable. On est en semi-décidable. Le spécifieur doit intervenir dans le processus de preuve)
  - des « contrôleurs de modèles » (model-checkers)
  - des animateurs de spécification

On utilise aussi le terme « outils » pour dénoter les langages utilisés ou encore les « notations » (ce terme mériterait une explicitation). Ainsi les « réseaux de Petri », les « automates de Harel » (des automates structurés) ou même le langage Pascal, Java, etc. seront considérés comme des outils.

Enfin, on trouve aussi : « Une méthode est un ensemble de concepts, langage, outils ».

Remarquons que le terme « méthodologie » est plus à la mode que le terme « méthode ». Mais si on s'en tient à l'étymologie, la méthodologie est « l'étude des méthodes ». Le dictionnaire de Lalande nous dit : « Subdivision de la Logique, ayant pour objet l'étude a posteriori des méthodes, et plus spécialement d'ordinaire, celle des méthodes scientifiques. Kant a opposé la Méthodologie à l'ensemble de la Logique (...) ».

[modifier] Exemples

[modifier] L'Analyse fonctionnelle descendante (SADT)

SADT dispose d'un langage avec un vocabulaire d'éléments graphiques (boîtes, flèches, étiquettes) à syntaxe formelle (les flèches doivent être positionnées à certains endroits selon le type de flèches, une flèche qui « entre » dans une boîte qui est composée d'autres boîtes, doit entrer dans une de ces autres boîtes. Mais SADT n'a pas de sémantique claire (par exemple, que signifie le fait qu'une flèche sorte d'une boîte et entre dans une autre).

[modifier] La Méthode B

La « méthode de spécification formelle B » (de Jean-Raymond Abrial) ne donne pas explicitement une séquence de tâches à effectuer. Différentes approches peuvent être prises (les entreprises la pratiquant définissent souvent l'approche qui convient à leurs applications). Mais il faut respecter les obligations de B et celles-ci impliquent certaines séquences d'actions.

Les spécifications sont faites en utilisant le langage de la théorie des ensembles et la logique des prédicats du premier ordre.

La sémantique des opérations (des substitutions) est définie par un ensembles d'axiomes dits « axiomes des substitutions généralisées »).

B met en œuvre les travaux de Dijkstra (langage de commande gardé).

B consiste à faire un développement prouvé (preuve mathématique), à raffiner jusqu'à arriver à des « machines » dont les opérations sont écrites dans un langage « algorithmique » qui est traduit automatiquement en langage exécutable (C, ADA,...).

L'Atelier B est un Atelier de génie logiciel qui comprend (entre autres) :

un analyseur syntaxique
un vérificateur de typage
un générateur d'obligations de preuves (i.e. de théorèmes à prouver)
plusieurs prouveurs, dont un prouveur dit « La balbulette », distribué gratuitement
un animateur de spécifications
un éditeur de spécifications
des générateurs de code

[modifier] Validation de spécification

Quand on se demande si le texte formel « dit bien » ce que l'on veut qu'il dise, s'il « traduit » bien la demande informelle faite par celui qui commande le logiciel, on dit que l'on fait de la validation. La validation ne peut pas être automatisée.

[modifier] Formel vs rigoureux

Un prouveur fait un raisonnement formel. Un spécifieur qui fait comme le professeur de mathématiques qui dit « il est évident que » et saute des étapes dans ses preuves, fait un raisonnement rigoureux. Autre exemple : On peut faire une spécification formelle en B. Puis faire un développement (passage au code exécutable) rigoureux.

[modifier] L'écriture des commentaires d'une spécification formelle

Ceux-ci sont écrits en langage naturel, mais en évitant des irrégularités (source : Thèse de Y. Toussaint, Méthodes informatiques et linguistiques pour l'aide à la spécification de logiciel, oct. 1992, U.P.S. Toulouse).

Mais celles-ci ne sont pas toujours un défaut ! :