Un sistema formal que define el significado de un lenguaje de programación mediante reglas de inferencia que describen cómo las frases del programa cambian estados de ejecución o se evalúan a valores, típicamente presentado en estilos de paso pequeño (transición) o paso grande (evaluación).

Principio

El significado de un programa se captura por reglas concretas que transforman estados: a cada construcción sintáctica se le asignan reglas de transición o evaluación que determinan cómo evolucionan los estados en tiempo de ejecución o cómo las expresiones producen valores.

Demostración

Ejemplo paso pequeño: una relación s -> s' que reduce una expresión aritmética (p. ej. (1+2) → 3) o una asignación que actualiza un almacén (⟨x:=e,σ⟩ → ⟨skip,σ[x↦v]⟩ cuando e se evalúa a v). Ejemplo paso grande: un juicio de evaluación ⟨e,σ⟩ ⇓ v que relaciona directamente una expresión y un entorno con un valor (p. ej. ⟨1+2,σ⟩ ⇓ 3).

Aplicación incorrecta

Tratar las reglas operacionales como modelos de temporización de implementación (extraer números de rendimiento de pasos abstractos), o usar reglas de paso pequeño sin modelar interacciones externas no deterministas y luego concluir sobre el comportamiento observable I/O; confundir semántica operacional con equivalencia denotacional sin relacionar ambos formalismos.

Consecuencia

Proporciona una descripción precisa y mecanizable del comportamiento en tiempo de ejecución, útil para probar propiedades como seguridad de tipos, corrección de transformaciones de compilador (vía simulación/ correspondencia de pasos) y para construir intérpretes o generadores de pruebas directamente a partir de las reglas.

Inversión

Sustituir la descripción paso a paso por una explicación axiomática o denotacional: la semántica axiomática da reglas de prueba sobre aserciones (tripletas de Hoare) sin describir pasos de ejecución; la semántica denotacional asigna objetos matemáticos a frases en lugar de transiciones de estado.

Límite

Cubre descripciones formales de construcciones del lenguaje, máquinas abstractas y relaciones de evaluación. No modela por sí misma el uso de recursos (tiempo real/energía) salvo extensión, ni sustituye las preocupaciones empíricas de implementación; excluye descripciones informales en lenguaje natural sin reglas de inferencia formales.

Tensión semántica

Tensión con la semántica denotacional (significados matemáticos extensionales) y la semántica axiomática (obligaciones de prueba): la semántica operacional enfatiza secuencias concretas de cómputo mientras los enfoques competidores enfatizan significados matemáticos abstractos o aserciones de corrección.

Síntesis

La semántica operacional es el formalismo basado en reglas y pasos que hace explícita la ejecución del programa: especificando cómo cada construcción transforma estados o se evalúa a valores proporciona una base mecanizable para razonar sobre la ejecución, probar la corrección de transformaciones y construir intérpretes, dejando los modelos de observación y recursos a extensiones cuando se necesiten.