Précédent Remonter Suivant

Sémantique des langages de programmation

Cours : Pierre Lescanne (Pierre.Lescanne)

TP : Etienne Lozes (Etienne.Lozes)

Cours de base (30 h de cours, 30h de TD)

Présentation
Le but du cours est d'introduire les techniques classiques de modélisation sémantique des langages de programmation, en liaison avec les autres cours de Master, notamment ceux de Programmation et de Compilation. Ce cours ne nécessite pas de connaissances mathématiques préalables; il s'adresse à toute personne curieuse de comprendre la structure des langages de programmation et les bases conceptuelles de la compilation et de la vérification tout en ayant le désir d'abstraire certain concept appréhendé jusque là seulement de leur point de vue pragmatique.

Dans ce cours, on souhaite montrer qu'il est possible de donner une description mathématique rigoureuse de concepts introduits souvent informellement dans les cours de programmation:
les programmes sont des objets mathématiques comme les autres.
Les outils mathématiques nécessaires à cette description seront présentés au début du cours dans un cas restreint et complété au fur et à mesure des besoins.

Plan indicatif
L'objet de la sémantique est fondamentalement d'associer du sens à des composants d'un langage. Pour nous ce seront les différents éléments d'un programme. Le sens est un objet mathématique à définir, sur lequel on peut faire des manipulations formelles et des preuves.

Dans la première partie de ce cours, nous étudierons les concepts de la sémantique sur un langage impératif de type Pascal à savoir
Sémantique opérationnelle :
on associe à un programme la suite des états d'une machine (abstraite) qui l'exécute;

Sémantique dénotationnelle:
on associe à un programme la fonction mathématique qu'il calcule;

Sémantique axiomatique:
on associe à un programme l'ensemble des assertions logiques reliant ses sorties et ses entrées.
Ensuite nous aborderons les concepts fondamentaux de la sémantique sur le lambda-calcul où les problèmes apparaissent sur leur jours mathématique le plus pur. Ensuite, nous étudierons les calculs pour la mobilité et la communications, notamment le p-calcul. Nous nous inspirerons essentiellement des deux premiers livres



Bibliographie
Précédent Remonter Suivant