Sémantiques formelles de langages de programmation

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.

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.