Ê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
Cours associés (4)
CS-320: Computer language processing
We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language in
CS-452: Foundations of software
The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a progr
CS-550: Formal verification
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
Publications associées (85)
Personnes associées (20)