Sémantique Opérationnelle

Un formalisme qui définit la signification d'un langage de programmation au moyen de règles d'inférence décrivant comment les phrases du programme modifient les états d'exécution ou s'évaluent en valeurs, généralement présenté en style petits pas (transition) ou grands pas (évaluation).