Spécification

Image manquante
Symbole-ordinateur.png

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

La spécification engage dans une voie déterminée et définie. Ce choix n'est pas irréversible.

En biologie du développement la spécification peut être de trois types.

Autonome

Il n'y a pas d'influence des cellules ou du tissus voisins. Si on enlève un blastomère, la partie correspondante sur l'embryon est manquante. On constate que les cellules sont spécifiées de façon très précoce souvent avant leur migration.

L'identité de la cellule va lui être donnée par des déterminants cytoplasmiques qui se mettent en place au plus tard pendant la segmentions. On trouve ça essentiellement chez les invertébré qui ont un développement mosaïque.

Syncitiale

Chez les insectes surtout la spécification est syncitiale. Il y a une interaction entre des composés cytoplasmiques d'origine maternelle et les noyaux dans syncitium avant la formation des membranes cellulaire. Quand il y a cellularisation les cellules sont déjà déterminées. C'est la transition blastuléenne.

Conditionnée ou conditionnelle

Le devenir de la cellule est imposée par des interactions avec l'environnement. Rien n'est fixé au départ. Les positions relatives des cellules sont décisives lors du développement embryologique. L'ablation précoce d'un blastomère peut être supplées par les blastomères voisins. On parle de développement à régulation. Dans ce modèle les réarrangements cellulaires, les mouvements cellulaire accompagnent la spécification.

Ce mécanisme existe chez toutes les espèces mais il est prépondérant chez les vertébrés.

En informatique il s'agit d'une étape du développement d'un logiciel (ou d'un système informatique)

On distingue :

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

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).

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, le 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 (...) ».

Quelques exemples illustratifs :

SADT

SADT dispose d'un langage avec un vocabulaire d'éléments graphiques (boites, 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 boites, doit entrer dans une de ces autres boites. 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).

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 Dikstra (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 AGL (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 (voir b4free)
- un animateur de spécifications
- un éditeur de spécifications
- des générateurs de code

Vérification vs validation de spécification

Le vocabulaire n'est pas fixé. Mais, sur wikipedia, on trouve « vérification formelle ». 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 être le résultat d'un processus automatique, d'un processus formel. La vérification, par contre, peut être formelle.

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.

L'écriture des commentaires d'une spécification formelle

Ceux-ci sont écrits en langage naturel, mais en évitant des irrégularites(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 ! :