Sémantique à grande échelle : définition d'expressions et de commandes arithmétiques

Cette séance de cours se concentre sur la définition d'un langage de programmation simple et de sa sémantique à l'aide de la sémantique à grande échelle. L'instructeur commence par examiner le langage des expressions arithmétiques, qui comprend des constantes, des variables et des opérations telles que l'addition, la soustraction et la multiplication. La notation de ces expressions est établie pour simplifier la représentation du langage. La séance de cours passe ensuite au concept d'évaluations, qui sont des cartes partielles des variables aux nombres naturels, et discute des opérations comme «obtenir» et «définir» pour la gestion de ces évaluations. L'instructeur prouve plusieurs lemmes liés à ces opérations pour créer un élan pour des preuves ultérieures. La séance de cours introduit également un langage impératif simple qui comprend des commandes pour l'affectation, le séquençage, les conditions et les boucles. L'instructeur met l'accent sur les différences entre cette approche et les méthodes précédentes, en particulier dans la façon dont la sémantique à grande échelle est modélisée. La session se termine par le développement d'un optimiseur pour le langage, démontrant comment prouver son exactitude grâce à une induction structurée sur les commandes.