Semántica (informática)

En la teoría de los lenguajes de programación, la semántica es el estudio matemático riguroso del significado de los lenguajes de programación. La semántica asigna significado computacional a cadenas válidas en la sintaxis de un lenguaje de programación. Está estrechamente relacionado y, a menudo, se cruza con la semántica de las demostraciones matemáticas.

Semántica describe los procesos que sigue una computadora al ejecutar un programa en ese lenguaje específico. Esto se puede mostrar describiendo la relación entre la entrada y la salida de un programa, o una explicación de cómo se ejecutará el programa en una determinada plataforma, creando así un modelo de cálculo.

Historia

En 1967, Robert W. Floyd publica el artículo Asignación de significados a programas; su principal objetivo es "un estándar riguroso para las pruebas sobre programas informáticos, incluidas las pruebas de corrección, equivalencia y terminación". Floyd escribe además:

Una definición semántica de un lenguaje de programación, en nuestro enfoque, se basa en una definición sintáctica. Debe especificar cuál de las frases en un programa sintácticamente correcto representan comandos, y qué condiciones deben imponerse a una interpretación en el vecindario de cada comando.

In 1969, Tony Hoare publishes a paper on Hoare logic seeded by Floyd 's ideas, now sometimes collectively called axiomatic semantics.

En la década de 1970, surgieron los términos semántica operativa y semántica denotacional.

Descripción general

El campo de la semántica formal abarca todo lo siguiente:

• La definición de modelos semánticos
• Las relaciones entre diferentes modelos semánticos
• Las relaciones entre diferentes enfoques de significado
• La relación entre la computación y las estructuras matemáticas subyacentes de campos tales como lógica, teoría de conjuntos, teoría modelo, teoría de la categoría, etc.

Tiene estrechos vínculos con otras áreas de la informática, como el diseño de lenguajes de programación, la teoría de tipos, los compiladores e intérpretes, la verificación de programas y la verificación de modelos.

Aproximaciones

Existen muchos enfoques de la semántica formal; estos pertenecen a tres clases principales:

• Semántica denotacional, por lo que cada frase en el idioma se interpreta como denotación, es decir, un significado conceptual que puede ser pensado abstractamente. Tales denotaciones son a menudo objetos matemáticos que habitan un espacio matemático, pero no es un requisito que deben ser así. Como necesidad práctica, las denotaciones se describen usando alguna forma de notación matemática, que puede a su vez ser formalizado como un metalanguage denotacional. Por ejemplo, la semántica denotacional de los idiomas funcionales a menudo traduce el lenguaje en la teoría del dominio. Las descripciones semánticas denotacionales también pueden servir como traducciones compositivas de un lenguaje de programación en el metalanguage denotacional y se utilizan como base para diseñar compiladores.
• Semántica operacional, por lo que la ejecución del idioma se describe directamente (en lugar de por traducción). La semántica operativa corresponde flojamente a la interpretación, aunque de nuevo el "idioma de ejecución" del intérprete es generalmente un formalismo matemático. La semántica operativa puede definir una máquina abstracta (como la máquina SECD), y dar sentido a frases describiendo las transiciones que inducen en estados de la máquina. Alternativamente, como con el cálculo de lambda pura, la semántica operacional se puede definir mediante transformaciones sintácticas en frases del propio lenguaje;
• Semántica axiomática, por lo que uno da significado a frases describiendo el axiomas que se aplican a ellos. La semántica axiomática no hace distinción entre el significado de una frase y las fórmulas lógicas que la describen; su significado es exactamente lo que se puede probar en alguna lógica. El ejemplo canónico de la semántica axiomática es la lógica de Hoare.

Aparte de la elección entre enfoques denotacionales, operacionales o axiomáticos, la mayoría de las variaciones en los sistemas semánticos formales surgen de la elección de apoyar el formalismo matemático.

Variaciones

Algunas variaciones de la semántica formal incluyen las siguientes:

• Semántica de acción es un enfoque que trata de modularizar la semántica denotacional, dividiendo el proceso de formalización en dos capas (macro y microsemántica) y predefinir tres entidades semánticas (acciones, datos y rendimientos) para simplificar la especificación;
• Semántica algebraica es una forma de semántica axiomática basada en leyes algebraicas para describir y razonar sobre la semántica del programa de una manera formal. También apoya la semántica denotacional y la semántica operacional;
• Gramáticas atribuidas define sistemas que computan sistemáticamente "metadatos" (llamados atributos) para los diversos casos de la sintaxis del lenguaje. Las gramáticas de atributo se pueden entender como una semántica denotacional donde el idioma objetivo es simplemente el idioma original enriquecido con anotaciones de atributo. Aparte de la semántica formal, las gramáticas de atributos también se han utilizado para la generación de código en los compiladores, y para aumentar las gramáticas regulares o sin contexto con condiciones sensibles al contexto;
• Semántica (o "functorial") usa la teoría de la categoría como el formalismo matemático básico. Una semántica categórica generalmente se demuestra que corresponde a una semántica axiomática que da una presentación sintáctica de las estructuras categóricas. Además, la semántica denotacional suele ser el caso de una semántica general categórica;
• Concurrency semantics es un término completo para cualquier semántica formal que describe computaciones concurrentes. Los formalismos concurrentes históricamente importantes han incluido el modelo actor y el proceso calculi;
• Juego de semántica usa una metáfora inspirada en la teoría del juego;
• Semántica del transformador, desarrollado por Edsger W. Dijkstra, describe el significado de un fragmento de programa como la función que transforma una condición post a la condición previa necesaria para establecerlo.

Describir relaciones

Por diversas razones, uno podría desear describir las relaciones entre diferentes semánticas formales. Por ejemplo:

• Demostrar que una semántica operativa particular para un lenguaje satisface las fórmulas lógicas de una semántica axiomática para ese lenguaje. Tal prueba demuestra que es "sonido" razonar sobre un particular (operacional) estrategia de interpretación utilizando un determinado (axiomático) sistema de prueba.
• Para demostrar que la semántica operativa sobre una máquina de alto nivel está relacionada con una simulación con la semántica sobre una máquina de bajo nivel, por lo que la máquina abstracta de bajo nivel contiene operaciones más primitivas que la definición de máquina abstracta de alto nivel de un lenguaje dado. Tal prueba demuestra que la máquina de bajo nivel "realmente implementa" la máquina de alto nivel.

También es posible relacionar múltiples semánticas a través de abstracciones a través de la teoría de la interpretación abstracta.