Cours de sémantique

L'objectif de ce cours est d'introduire les étudiants aux différentes techniques utilisées pour décrire exactement le comportement des programmes. Ce cours est organisé en 6 séances de 2 heures, accompagnées de 6 séances de Travaux dirigés sur machine.

Première séance

La première séance a pour objectif de présenter la sémantique naturelle. Les notes de cours ont la forme d'un article d'une dizaine de pages, postscript compressé.

TD de la première séance

Dans ces TD, nous construisons des dérivations d'exécution pour plusieurs programmes. Nous tâcherons d'évaluer la taille de ces dérivations et nous verrons comment automatiser la construction. Nous nous reposerons sur l'utilisation d'un système de démonstration sur ordinateur appelé Jape. Ce système est disponible sur la majeure partie des machines Unix et MacIntosh. Nous utiliserons pour notre cours un fichier de configuration appelé little.jt (aussi en postscript compressé).

Deuxième séance

La deuxième séance a pour objectif de présenter la sémantique dénotationelle. Les notes de ce cours sont disponibles en postscript compressé.

TD de la deuxième séance

Dans ces TD, nous construisons un programme en Scheme qui implémente les différentes fonctions mathématiques décrite dans la première partie du cours. L'objectif est donc de construire:

1. Des environnements, c'est à dire des fonctions partielles des noms de variable (des symboles de scheme) vers les valeurs entières.
   1. L'environnement vide sera représenté par une fonction à un argument qui retourne toujours une erreur.
   2. Un environnement peut être modifié grâce à la fonction update, qui reçoit, dans cet ordre, un environnement e, un nom de variable v, et une valeur entière n, et retourne un environnement qui se comporte comme l'environnement e partout sauf en la variable v, pour laquelle ce nouvel environnement retourne n.
2. La sémantique des expressions arithmétiques sera représentée par une fonction denote-a qui prend un argument e qui est une expression et retourne une fonction des environnements vers les valeurs entières. La fonction denote-a représente la fonction écrite dans le cours avec le A majuscule en lettre ronde.
3. La sémantique des expressions booléennes sera représentée par une fonction denote-b qui prend un argument e qui est une expression booléenne et retourne une fonction des environnements vers l'ensemble {true, false}. La fonction denote-b représente la fonction écrite dans le cours avec le B majuscule en lettre ronde.
4. La sémantique des instructions sera représentée par une fonction denote-i qui prend un argument i qui est une instruction et retourne une fonction des environnements vers les environnements. La fonction denote-i représente la fonction écrite dans le cours avec le I majuscule en lettre ronde.
5. Pour la sémantique des instructions de boucle on se reposera sur une fonction fix-point qui prend en argument une fonction F d'un ensemble de fonctions dans lui-même et qui retourne un élement invariant par cette fonction, c'est à dire que mathématiquement les valeurs fix-point(F) et F(fixpoint(F)) sont deux fonctions égales en tout point. On étudiera également les moyens de construire cette fonction fix-point en scheme.

Troisième séance

La troisième séance a pour objectif de montrer les correspondances entre les deux descriptions sémantiques du langage. Les notes de ce cours sont disponibles en postscript compressé

TD de la troisième séance

Dans cette séance, nous montrerons comment décrire la sémantique naturelle pour un langage fonctionnel pur (liaison statique et appel par valeurs) en utilisant le programme Jape déjà utilisé en première séance de TD.

Alternativement, nous pourrons utiliser la sémantique naturelle comme ligne guide pour écrire un interprète pour ce langage fonctionnel en scheme.

La solution de ces TD est disponible: sémantique naturelle en format Jape (aussi en postscript compressé), ou bien programme scheme pour l'interprète du langage fonctionnel.

quatrieme seance

Notes du cours

Exercices

Voici quelques exercices qui auraient pu servir d'examen exercices2.ps.gz et leurs reponses2.ps.gz.