Langage de spécification

Les langages de spécification ne sont généralement pas exécutés directement. Ils sont destinés à décrire le quoi, pas le comment. En effet, il est considéré comme une erreur si une spécification d'exigence est encombrée de détail d'implémentation non nécessaire.

Une hypothèse fondamentale commune à de nombreuses approches de spécifications est que les programmes sont modélisés sous forme de structures algébriques ou de structures théoriques des modèles comprenant une collection d'ensembles de valeurs de données ainsi que des fonctions sur ces ensembles. Ce niveau d'abstraction coïncide avec l'idée que l'exactitude du comportement entrée/sortie d'un programme prime sur toutes ses autres propriétés.

Dans l'approche de la spécification orientée sur les propriétés (pris e.g. par la CASL (en), les spécifications des programmes consistent principalement en axiomes logiques, généralement dans un système logique dans lequel l'égalité joue un rôle prépondérant, décrivant les propriétés que les fonctions doivent satisfaire - souvent uniquement par leurs interrelations. Contrairement à ce que l'on appelle la spécification orientée modèle dans les frameworks tel que VDM et Z, qui consistent en une simple réalisation du comportement requis.

Les spécifications doivent faire l'objet d'un processus d'affinement (le remplissage des détails de la mise en œuvre) avant de pouvoir être réellement mises en œuvre. Le résultat d'un tel processus de raffinement est un algorithme exécutable, qui est soit formulé dans un langage de programmation, soit dans un sous-ensemble exécutable du langage de spécification en question. Par exemple, les pipelines de Hartmann (en), lorsqu'ils sont correctement appliqués, peuvent être considérés comme une spécification de flux de données qui est directement exécutable. Un autre exemple est le modèle d'acteur qui n'a pas de contenu d'application spécifique et doit être spécialisé pour être exécutable.

Une utilisation importante des langages de spécification permet de créer des preuves de la correction d'un programme (voir la démonstration automatique de théorèmes).

• LOTOS
• E-LOTOS
• VDM
• Z
• Vérification de modèles
• SDL
• Coq

• UML
• SDL

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Specification language » (voir la liste des auteurs).