Sémantiques formelles de langages de programmation

FUNDP-INFO-3106 -- J.-M. Jacquet -- 30-0-0 -- Cours de 3ème cycle

Objectif

L'utilité des sémantiques formelles comme modèles mathématiques servant de base à la compréhension et au raisonnement de programmes est largement admise. Ce cours se propose d'étudier les notions mathématiques, les techniques et les concepts qui les sous-tendent ainsi que de les exemplifier au travers de l'étude de langages ou de fragments de langages.

Prérequis

Aucun

Contenu

Trois types principaux de sémantiques ont émergés des recherches:

1. Les sémantiques opérationnelles décrivent les éxecutions de programmes en termes (abstraits) d'éxecutions sur une machine abstraite. Elles font suite aux travaux de G. Plotkin sur les ``structural operational semantics''.
2. Les sémantiques dénotationnelles décrivent les programmes d'une facon compositionnelle et sur base de structures mathématiques riches telles que les treillis complets ou les espaces métriques complets. Elles font suite aux travaux de C. Strachey, D. Scott, J.W. de Bakker et M. Nivat, pour n'en citer que quelques uns.
3. Les sémantiques axiomatiques caractérisent les mécanismes de programmation au moyen de règles d'une théorie de preuve d'une certaine logique. Elles font suite aux travaux de R. Floyd et de C.A.R. Hoare.

Il serait erroné d'opposer ces sémantiques. Chacune possède son utilité. Ainsi, une sémantique operationnelle claire est très utile pour concevoir une implémentation, les sémantiques axiomatiques offrent des systèmes de preuves élégants pour développer et vérifier les programmes, et les sémantiques dénotationnelles sont à l'origine des techniques les plus sophistiquées.

Etudier ces sémantiques séparément serait aussi une erreur. Ainsi, établir la correction d'une sémantique axiomatique requiert la connaissance à priori d'une sémantique opérationnelle, voire dénotationnelle. De même, l'argumentation de la correction d'une implémentation par rapport à une sémantique dénotationnelle requiert le passage par une sémantique opérationnelle et son lien avec la sémantique denotationnelle considérée. Le problème se pose alors naturellement de distinguer parmi les differents types de sémantiques celles qui correspondent le plus étroitement aux autres. On est alors amené à parler naturellement de sémantiques complètement abstraites.

Le but du cours est de donner les éléments de base nécessaires au développement de ces sémantiques, de les étudier et de les comparer sur base de langages simples mais incluant des mécanismes fondamentaux.

Le plan du cours proposé est:

1. Notions préliminaires
   1. Relations bien fondées et induction
   2. Cpo, Complete lattice, fonctions continues et monotones, théorème de Knaster-Tarski
   3. Espaces métriques complets, contractions, théorème de Banach

2. : Langage impératif simple (comportant assignation, choix, composition séquentielle, procédure avec définition récursive)
   1. Sémantique opérationnelle
   2. Sémantique algébrique
   3. Sémantique dénotationnelle
   4. Comparaison
      1. Cohérence et complétude de la sémantique axiomatique
      2. Correction de la sémantique dénotationnelle

3. : + communication synchrone
   1. Sémantique opérationnelle
   2. Sémantique algébrique
   3. Sémantique dénotationnelle
   4. Comparaison
      1. Cohérence et complétude de la sémantique axiomatique
      2. Correction de la sémantique dénotationnelle

4. : + communication asynchrone
   1. Sémantique opérationnelle
   2. Sémantique algébrique
   3. Sémantique dénotationnelle
   4. Comparaison
      1. Cohérence et complétude de la sémantique axiomatique
      2. Correction de la sémantique dénotationnelle

5. Sémantiques complètement abstraites
   1. Pour
   2. Pour
   3. Pour

Pédagogie

Le cours est dispensé par l'enseignant; il est agrémenté d'exercices proposés afin de tester la compréhension et d'approfondir les connaissances.

L'examen est oral.

Références

27
J. de Bakker and E. de Vink . Control Flow Semantics. The MIT Press, 1996.

28
C. Gunter. Semantics of Programming Languages. The MIT Press, 1992.

29
M. Smith. Topology. Handbook of Logic in Computer Science, vol 1, Oxford Science Publications, 1992.

30
G. Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993.