Spécification (informatique)

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

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

Cet article ou cette section doit être recyclé. Sa qualité devrait être largement améliorée en le réorganisant et en le clarifiant.
L'utilisateur qui appose ce bandeau est invité à énoncer les points à améliorer en page de discussion.

Cet article, bien que respectant dans une certaine mesure la neutralité de point de vue, est jugé trop incomplet dans son développement ou dans l'expression des concepts et des idées. Son contenu est donc à considérer avec précaution. Pour toute information complémentaire, veuillez consulter sa page de discussion et la liste des articles incomplets.

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 À lire
- 7.1 Liens externes
  - 7.1.1 Prouveurs
  - 7.1.2 Model checkers

[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
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

Celui qui prouve fait un raisonnement formel. Celui qui spécifie en disant « il est évident que » et en sautant 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

Les commentaires d'une spécification formelle sont écrits en langage naturel, mais en évitant les 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 !

le bruit, information non nécessaire au moment où elle est donnée
le silence, notions introduites sans définition (un peu comme une non-déclaration de variable)
la contradiction
la sur-spécification : en dire trop. Par exemple, traiter d'implantation alors qu'on n'a pas spécifié la fonction que l'on veut implanter.
l'ambiguïté, c'est-à-dire un énoncé à interprétations multiples
la référence en avant (n'est pas forcément mauvaise !), on mentionne des concepts dont la définition sera fournie plus loin. Un sommaire est fait de référence en avant !