Sémantique (informatique) - Semantics (computer science)
Dans la théorie des langages de programmation , la sémantique est le domaine concerné par l'étude mathématique rigoureuse de la signification des langages de programmation . Il le fait en évaluant la signification des chaînes syntaxiquement valides définies par un langage de programmation spécifique, montrant le calcul impliqué. Dans un tel cas où l'évaluation porterait sur des chaînes syntaxiquement invalides, le résultat serait un non-calcul. La sémantique décrit les processus suivis par un ordinateur lors de l'exécution d'un programme dans ce langage spécifique. Cela peut être montré en décrivant la relation entre l'entrée et la sortie d'un programme, ou une explication de la façon dont le programme sera exécuté sur une certaine plate-forme, créant ainsi un modèle de calcul .
Aperçu
Le domaine de la sémantique formelle englobe tous les éléments suivants :
- La définition des modèles sémantiques
- Les relations entre les différents modèles sémantiques
- Les relations entre différentes approches du sens
- La relation entre le calcul et les structures mathématiques sous - jacentes de domaines tels que la logique , la théorie des ensembles , théorie des modèles , la théorie des catégories , etc.
Il entretient des liens étroits avec d'autres domaines de l' informatique tels que la conception de langages de programmation , la théorie des types , les compilateurs et interprètes , la vérification de programmes et la vérification de modèles .
Approches
Il existe de nombreuses approches de la sémantique formelle ; ceux-ci appartiennent à trois grandes classes :
- Sémantique dénotationnelle , où chaque phrase de la langue est interprétée comme une dénotation , c'est-à-dire une signification conceptuelle qui peut être pensée de manière abstraite. De telles dénotations sont souvent des objets mathématiques habitant un espace mathématique, mais ce n'est pas une exigence qu'elles le soient. En tant que nécessité pratique, les dénotations sont décrites en utilisant une certaine forme de notation mathématique, qui peut à son tour être formalisée comme un métalangage dénotationnel. Par exemple, la sémantique dénotationnelle des langages fonctionnels traduit souvent le langage en théorie des domaines . Les descriptions sémantiques dénotationnelles peuvent également servir de traductions compositionnelles d'un langage de programmation vers le métalangage dénotationnel et servir de base à la conception de compilateurs .
- Sémantique opérationnelle , où l'exécution du langage est décrite directement (plutôt que par traduction). La sémantique opérationnelle correspond vaguement à l' interprétation , bien qu'à nouveau le « langage de mise en œuvre » de l'interprète soit généralement un formalisme mathématique. La sémantique opérationnelle peut définir une machine abstraite (telle que la machine SECD ), et donner un sens aux phrases en décrivant les transitions qu'elles induisent sur les états de la machine. Alternativement, comme avec le calcul lambda pur, la sémantique opérationnelle peut être définie via des transformations syntaxiques sur des phrases de la langue elle-même ;
- Sémantique axiomatique , où l'on donne un sens aux phrases en décrivant les axiomes qui s'y appliquent. La sémantique axiomatique ne fait aucune distinction entre le sens d'une phrase et les formules logiques qui la décrivent ; sa signification est exactement ce qui peut être prouvé à son sujet dans une certaine logique. L'exemple canonique de la sémantique axiomatique est la logique de Hoare .
Outre le choix entre les approches dénotationnelles, opérationnelles ou axiomatiques, la plupart des variations dans les systèmes sémantiques formels découlent du choix de soutenir le formalisme mathématique.
Variantes
Certaines variantes de la sémantique formelle sont les suivantes :
- La sémantique d'action est une approche qui essaie de modulariser la sémantique dénotationnelle, en divisant le processus de formalisation en deux couches (macro et microsémantique) et en prédéfinissant trois entités sémantiques (actions, données et producteurs) pour simplifier la spécification ;
- La sémantique algébrique est une forme de sémantique axiomatique surbase algébrique des lois pour décrire et raisonner sur la sémantique du programme dans une formelle manière;
- Les grammaires d'attributs définissent des systèmes qui calculent systématiquement des « métadonnées » (appelées attributs ) pour les différents cas de la syntaxe du langage . Les grammaires d'attributs peuvent être comprises comme une sémantique dénotationnelle où la langue cible est simplement la langue d'origine enrichie d'annotations d'attributs. Outre la sémantique formelle, les grammaires d'attributs ont également été utilisées pour la génération de code dans les compilateurs et pour augmenter les grammaires régulières ou sans contexte avec des conditions contextuelles ;
- La sémantique catégorique (ou « fonctionnelle ») utilise la théorie des catégories comme formalisme mathématique de base. Il est généralement prouvé qu'une sémantique catégorique correspond à une sémantique axiomatique qui donne une présentation syntaxique des structures catégoriques. De plus, la sémantique dénotationnelle est souvent des instances d'une sémantique catégorique générale,
- La sémantique de concurrence est un terme fourre-tout pour toute sémantique formelle qui décrit des calculs concurrents. Les formalismes concurrents d'importance historique ont inclus le modèle d'acteur et les calculs de processus ;
- La sémantique des jeux utilise une métaphore inspirée de la théorie des jeux .
- La sémantique des transformateurs de prédicats , développée par Edsger W. Dijkstra , décrit la signification d'un fragment de programme comme la fonction transformant une post - condition en précondition nécessaire pour l'établir.
Décrire les relations
Pour diverses raisons, on peut souhaiter décrire les relations entre différentes sémantiques formelles. Par exemple:
- Prouver qu'une sémantique opérationnelle particulière pour une langue satisfait les formules logiques d'une sémantique axiomatique pour cette langue. Une telle preuve démontre qu'il est « bon » de raisonner sur une stratégie d'interprétation (opérationnelle) particulière en utilisant un système de preuve (axiomatique) particulier .
- Prouver que la sémantique opérationnelle sur une machine de haut niveau est liée par une simulation avec la sémantique sur une machine de bas niveau, la machine abstraite de bas niveau contenant plus d'opérations primitives que la définition de machine abstraite de haut niveau d'un langage donné. Une telle preuve démontre que la machine de bas niveau « met fidèlement en œuvre » la machine de haut niveau.
Il est également possible de relier plusieurs sémantiques à travers des abstractions via la théorie de l'interprétation abstraite .
Histoire
Robert W. Floyd est crédité d'avoir fondé le domaine de la sémantique des langages de programmation dans Floyd (1967) .
Voir également
- Sémantique computationnelle
- Sémantique formelle (logique)
- Sémantique formelle (linguistique)
- Ontologie
- Ontologie (sciences de l'information)
- Équivalence sémantique
- Technologie sémantique
Les références
Lectures complémentaires
- Manuels
- Floyd, Robert W. (1967). « Attribuer des significations aux programmes » (PDF) . Dans Schwartz, JT (éd.). Aspects mathématiques de l'informatique . Actes du colloque sur les mathématiques appliquées. 19 . Société mathématique américaine. p. 19-32. ISBN 0821867288.
- Hennessy, M. (1990). La sémantique des langages de programmation : une introduction élémentaire utilisant la sémantique opérationnelle structurelle . Wiley. ISBN 978-0-471-92772-3.
- Tennent, Robert D. (1991). Sémantique des langages de programmation . Prentice Hall. ISBN 978-0-13-805599-8.
- Gunter, Carl (1992). Sémantique des langages de programmation . Presse MIT. ISBN 0-262-07143-6.
- Nielson, RH ; Nielson, Flemming (1992). Sémantique avec applications : une introduction formelle (PDF) . Wiley. ISBN 978-0-471-92980-2.
- Winskel, Glynn (1993). La sémantique formelle des langages de programmation : une introduction . Presse MIT. ISBN 0-262-73103-7.
- Mitchell, John C. (1995). Fondements des langages de programmation (Postscript) .
- Slonneger, Kenneth ; Kurtz, Barry L. (1995). Syntaxe formelle et sémantique des langages de programmation . Addison-Wesley. ISBN 0-201-65697-3.
- Reynolds, John C. (1998). Théories des langages de programmation . La presse de l'Universite de Cambridge. ISBN 0-521-59414-6.
- Harper, Robert (2006). Fondements pratiques des langages de programmation (PDF) . Archivé de l'original (PDF) le 2007-06-27. (Document de travail)
- Nielson, RH ; Nielson, Flemming (2007). Sémantique avec applications : un apéritif . Springer. ISBN 978-1-84628-692-6.
- Souche, Aaron (2014). Fondements du langage de programmation . Wiley. ISBN 978-1-118-00747-1.
- Krishnamurthi, Shriram (2012). « Langues de programmation : application et interprétation » (2e éd.).
- Notes de lecture
- Winskel, Glynn. "Sémantique dénotationnelle" (PDF) . Université de Cambridge.
Liens externes
- Aaby, Anthony (2004). Introduction aux langages de programmation . Archivé de l'original le 2015-06-19.CS1 maint : bot : état de l'URL d'origine inconnu ( lien ) Sémantique.