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).

Principe

Le sens d'un programme est capté par des règles concrètes de transformation d'états : chaque construction syntaxique se voit attribuer des règles de transition ou d'évaluation qui déterminent l'évolution des états d'exécution ou la production de valeurs par les expressions.

Démonstration

Exemple petits pas : une relation s -> s' qui réduit une expression arithmétique (p. ex. (1+2) → 3) ou une affectation qui met à jour un magasin (⟨x:=e,σ⟩ → ⟨skip,σ[x↦v]⟩ quand e s'évalue en v). Exemple grands pas : un jugement d'évaluation ⟨e,σ⟩ ⇓ v qui relie directement une expression et un environnement à une valeur (p. ex. ⟨1+2,σ⟩ ⇓ 3).

Mauvaise application

Considérer les règles opérationnelles comme des modèles de performance d'implémentation (en déduire des temps d'exécution), ou employer des règles petits pas sans modéliser les interactions externes non déterministes puis tirer des conclusions sur le comportement observable ; confondre sémantique opérationnelle et preuves d'équivalence dénotationale sans établir de lien formel.

Conséquence

Fournit une description précise et mécanisable du comportement à l'exécution utile pour prouver des propriétés telles que la solidité des types, la correction des transformations de compilateur (via simulation/correspondance de pas), et pour construire des interprètes ou générateurs de tests directement à partir des règles.

Inversion

Remplacer la description pas à pas par un exposé axiomatique ou dénotationnel : la sémantique axiomatique fournit des règles de preuve sur des assertions (triplets de Hoare) sans décrire les étapes d'exécution ; la sémantique dénotationnelle associe des objets mathématiques aux phrases plutôt que des transitions d'état.

Limite

Couvre les descriptions formelles des constructions de langage, des machines abstraites et des relations d'évaluation. Ne modélise pas en soi l'usage des ressources (temps réel/énergie) sauf extension, et ne remplace pas les préoccupations d'implémentation empiriques ; exclut les descriptions informelles en langue naturelle dépourvues de règles d'inférence formelles.

Tension sémantique

Tension avec la sémantique dénotationnelle (sens mathématique extensionnel) et la sémantique axiomatique (obligations de preuve) : la sémantique opérationnelle met l'accent sur les séquences concrètes de calcul tandis que les autres privilégient la signification mathématique abstraite ou les assertions de correction.

Synthèse

La sémantique opérationnelle est le formalisme fondé sur des règles et les pas qui rend explicite l'exécution des programmes : en spécifiant comment chaque construction transforme les états ou s'évalue en valeurs, elle offre une base mécanisable pour raisonner sur l'exécution, prouver la correction des transformations et construire des interprètes, en laissant au besoin les modèles d'observation et de ressources à des extensions dédiées.