Semántica Operacional

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