(2018 : 930 - Sémantique des langages de programmation. Exemples.)
L’objectif est de formaliser ce qu’est un programme : introduction des sémantiques opérationelle et dénotationelle, dans le but de pouvoir faire des preuves de programmes, des preuves d’équivalence, des preuves de correction de traduction. Ces notions sont typiquement introduites sur un langage de programmation (impératif) jouet. On peut tout à fait se limiter à un langage qui ne nécessite pas l’introduction des CPOs et des théorèmes de point fixe généraux. En revanche, on s’attend ici à ce que les liens entre sémantique opérationelle et dénotationelle soient étudiés (toujours dans le cas d’un langage jouet). Il est aussi important que la leçon présente des exemples d’utilisation des notions introduites, comme des preuves d’équivalence de programmes ou des preuves de correction de programmes.