Semántica (informática) - Semantics (computer science)

En la teoría de los lenguajes de programación , la semántica es el campo que se ocupa del estudio matemático riguroso del significado de los lenguajes de programación . Lo hace evaluando el significado de cadenas sintácticamente válidas definidas por un lenguaje de programación específico, mostrando el cálculo involucrado. En el caso de que la evaluación sea de cadenas sintácticamente inválidas, el resultado sería no computación. La 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 plataforma determinada , creando así un modelo de cálculo .

Visió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 del significado
  • La relación entre la computación y las estructuras matemáticas subyacentes de campos como la lógica , la teoría de conjuntos , la teoría de modelos , la teoría de categorías , 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 .

Enfoques

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

  • Semántica denotacional , según la cual cada frase del lenguaje se interpreta como una denotación , es decir, un significado conceptual que se puede pensar de manera abstracta. Tales denotaciones son a menudo objetos matemáticos que habitan un espacio matemático, pero no es un requisito que deban serlo. Como una necesidad práctica, las denotaciones se describen utilizando alguna forma de notación matemática, que a su vez puede formalizarse como un metalenguaje denotacional. Por ejemplo, la semántica denotacional de los lenguajes funcionales a menudo traduce el lenguaje en teoría de dominio . Las descripciones semánticas denotacionales también pueden servir como traducciones composicionales de un lenguaje de programación al metalenguaje denotacional y usarse como base para diseñar compiladores .
  • Semántica operacional , por la cual la ejecución del lenguaje se describe directamente (en lugar de por traducción). La semántica operacional se corresponde libremente con la interpretación , aunque nuevamente el "lenguaje de implementació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 significado a frases al describir las transiciones que inducen en los estados de la máquina. Alternativamente, como con el cálculo lambda puro, la semántica operacional puede definirse mediante transformaciones sintácticas en frases del lenguaje mismo;
  • Semántica axiomática , mediante la cual se da significado a las frases describiendo los axiomas que se aplican a ellas. La semántica axiomática no distingue entre el significado de una frase y las fórmulas lógicas que la describen; su significado es exactamente lo que se puede probar sobre él en alguna lógica. El ejemplo canónico de 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 del formalismo matemático de apoyo.

Variaciones

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

Describiendo relaciones

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

  • Demostrar que una semántica operacional particular para un lenguaje satisface las fórmulas lógicas de una semántica axiomática para ese lenguaje. Tal prueba demuestra que es "sólido" razonar sobre una estrategia de interpretación particular (operativa) utilizando un sistema de prueba particular (axiomático) .
  • Demostrar que la semántica operativa sobre una máquina de alto nivel está relacionada mediante 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 más operaciones 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 "implementa fielmente" la máquina de alto nivel.

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

Historia

A Robert W. Floyd se le atribuye la fundación del campo de la semántica del lenguaje de programación en Floyd (1967) .

Ver también

Referencias

Otras lecturas

Libros de texto
Notas de lectura

enlaces externos