Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Langage de spécification
Résumé
Un langage de spécification est un Langage formel en Informatique utilisé pendant l'analyse systémique, l'analyse des exigences et la conception des systèmes pour décrire un système à un niveau beaucoup plus élevé qu'un langage de programmation, qui est utilisé pour produire un code exécutable pour un système.
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 , 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 , 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.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Proximité ontologique