La semántica operativa es una categoría de la semántica del lenguaje de programación formal en la que ciertas propiedades deseadas de un programa , como la corrección, la seguridad o la seguridad, se verifican mediante la construcción de pruebas a partir de declaraciones lógicas sobre su ejecución y procedimientos, en lugar de adjuntar significados matemáticos a sus términos. ( semántica denotacional ). La semántica operativa se clasifica en dos categorías: la semántica operativa estructural (o semántica de pasos pequeños ) describe formalmente cómo los pasos individuales de un cálculotener lugar en un sistema basado en computadora; por oposición, la semántica natural (o semántica de grandes pasos ) describe cómo se obtienen los resultados generales de las ejecuciones. Otros enfoques para proporcionar una semántica formal de los lenguajes de programación incluyen la semántica axiomática y la semántica denotacional .
La semántica operativa de un lenguaje de programación describe cómo se interpreta un programa válido como secuencias de pasos computacionales. Estas secuencias son entonces el significado del programa. En el contexto de la programación funcional , el paso final de una secuencia de terminación devuelve el valor del programa. (En general, puede haber muchos valores de retorno para un solo programa, porque el programa podría ser no determinista , e incluso para un programa determinista puede haber muchas secuencias de cálculo, ya que la semántica puede no especificar exactamente qué secuencia de operaciones llega a ese valor).
Quizás la primera encarnación formal de la semántica operativa fue el uso del cálculo lambda para definir la semántica de Lisp . [1] Las máquinas abstractas en la tradición de la máquina SECD también están estrechamente relacionadas.
El concepto de semántica operacional se utilizó por primera vez para definir la semántica de Algol 68 . La siguiente declaración es una cita del informe ALGOL 68 revisado:
El significado de un programa en el lenguaje estricto se explica en términos de una computadora hipotética que realiza el conjunto de acciones que constituyen la elaboración de ese programa. ( Algol68 , Sección 2)
El primer uso del término "semántica operativa" en su significado actual se atribuye a Dana Scott ( Plotkin04 ). Lo que sigue es una cita del artículo seminal de Scott sobre semántica formal, en el que menciona los aspectos "operativos" de la semántica.