Sémantique (programmation)
Ce qu'un programme signifie, c'est-à-dire ce qu'il fait quand il s'exécute. À distinguer de la syntaxe (son apparence). Trois approches formelles pour la spécifier : opérationnelle, dénotationnelle, axiomatique.
Opérationnelle : le programme est une machine à états et la sémantique décrit l'effet de chaque pas (machine SECD, interprétation abstraite). Dénotationnelle : le programme est une fonction mathématique (Scott et Strachey, années 1970). Axiomatique : le programme est un ensemble d'énoncés logiques sur l'état (logique de Hoare, logique de séparation). Utile en pratique pour la conception de compilateurs, la vérification formelle et la conception de langages. Le comportement indéfini de C/C++, c'est « là où la sémantique ne dit rien » : le compilateur a alors le droit de faire disparaître ces cas à l'optimisation.