Ê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.
Catégorie
Sémantique des langages de programmation
Résumé
En informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques.
Comme en linguistique, la sémantique, appliquée aux langages de programmation, désigne le lien entre un signifiant, le programme, et un signifié, objet mathématique. L'objet mathématique dépend des propriétés à connaître du programme.
La sémantique est également le lien entre :
le langage signifiant : le langage de programmation
le langage signifié : logique de Hoare, automates...
Les sémantiques les plus couramment utilisées pour donner du sens à un langage de programmation sont :
sémantique opérationnelle
sémantique dénotationnelle
sémantique axiomatique.
Sémantique opérationnelle
En sémantique opérationnelle, la signification d’un programme est la suite des états de la machine qui exécute le programme. Autrement dit, un programme est considéré comme la description d’un système de transition d'états.
Dans cette sémantique, les programmes :
a=1; b=0
et
a=1;
b=0
sont équivalents car ils ont la même signification.
Par contre le programme :
b=0; a=1
ne leur est pas équivalent. En effet, même si le résultat final est le même, les actions d'affectation de valeurs aux variables a et b n’ont pas lieu dans le même ordre.
Il est possible d'abstraire cette sémantique en n’observant qu’une partie de la mémoire de la machine, telle que :
les interactions du programme avec l’extérieur
la trace du programme.
Sémantique dénotationnelle
Initiée par Christopher Strachey et Dana Scott, la sémantique dénotationnelle est une approche dans laquelle une fonction mathématique appelée dénotation est associée à chaque programme, et représente en quelque sorte son effet, sa signification. Cette fonction prend par exemple pour argument l’état de la mémoire avant exécution, et a pour résultat l’état après exécution.
Dans cette sémantique, tous les exemples donnés ci-dessus pour la sémantique opérationnelle sont équivalents, mais le programme :
a=1;
b=1;
ne leur est pas équivalent.
À 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.