Semántica de lenguajes de programación (formal, informática), qué es

Seguimos profundizando en la semántica, esta vez la vamos a relacionar con la computación obviamente, que es nuestro campo directo de estudio, hasta lograr saber lo que significa (definición, concepto), sus características e implicaciones.

En el campo de la informática teórica, el término semántica formal se refiere a los modelos matemáticos que definen formalmente los lenguajes de programación o, más generalmente, la computación en sí.
Como en la lingüística, la semántica, aplicada a los lenguajes de programación, designa el vínculo entre un significante, el programa, y un significado, un objeto matemático. El objeto matemático depende de las propiedades a conocer del programa.

Enfoques

Existen múltiples enfoques para el estudio de esta semántica; que se dividen en 3 categorías principales:

Semántica denotacional

Se ocupa de formalizar la ejecución de las instrucciones de un lenguaje de programación utilizando objetos matemáticos, denominados denotaciones, que describen su significado y por tanto su ejecución. Generalmente esta semántica debe ser composicional: la denotación de una parte del programa debe construirse a partir de sus sub-instrucciones.

Iniciada o creada por Christopher Strachey y Dana Scott, la semántica denotacional es un enfoque en el que una función matemática llamada denotación se asocia con cada programa y, de alguna manera, representa su efecto, su significado. Esta función toma, por ejemplo, el estado de la memoria antes de la ejecución y da como resultado el estado después de la ejecución.

Existen varias variantes de la semántica denotacional, una de las más famosas es la semántica denotacional por continuación que, en lugar de asociar un programa a una función que transforma la memoria, la asocia a una función que transforma la continuación (el futuro ) de la máquina después de la ejecución del programa. En otras palabras, la semántica denotacional por continuación funciona a la inversa del programa, considera lo que sucede después de una instrucción para deducir de ella lo que debe suceder antes de esta instrucción.

Uno de los aspectos importantes de la semántica denotacional es la propiedad de composicionalidad: la denotación de un programa se obtiene combinando las denotaciones de sus constituyentes.

Semántica operativa

Describe la ejecución de un programa a través de transiciones definidas directamente en el lenguaje del programa. Este tipo de formalismo es conceptualmente similar a la interpretación real donde tenemos una máquina abstracta y las instrucciones aplican transiciones de estado en esta máquina. Por lo tanto, tenemos una secuencia de pasos computacionales definida para cada programa (que puede ser no determinista) y que generalmente se genera aplicando un conjunto de reglas de inferencia en el propio conjunto de instrucciones.

Semántica axiomática

Se basa en identificar el estado del cálculo pero usa predicados lógicos para definir el estado actual. Este tipo de semántica no distingue la verdad implícita en un fragmento de código y su significado: son exactamente lo mismo. Generalmente se usa para intentar verificar la corrección de programas y su ejemplo más llamativo y clásico es la lógica de Floyd.

En semántica axiomática, el programa no es más que un transformador de propiedades lógicas en el estado de la memoria: si tenemos p verdadero antes de la ejecución, entonces tenemos q verdadero después. Ya no estamos interesados ​​en el estado preciso de la memoria mientras sepamos si la propiedad se mantiene.

Si la propiedad que nos interesa es saber si un y b son positivos después de la ejecución del programa, entonces todos los ejemplos anteriores son equivalentes en el sentido de que cualquiera que sea el estado de la máquina antes de la ejecución del programa, la línea la salida se sostiene.

Relación entre las diferentes semánticas

Estas tres semánticas, como sugieren los ejemplos, no son completamente independientes entre sí, de hecho:

Dos programas sintácticamente equivalentes son operacionalmente equivalentes;
dos programas operacionalmente equivalentes son denotacionalmente equivalentes;
y dos programas denotacionalmente equivalentes son axiomáticamente equivalentes.
Pero lo contrario está mal.

Por tanto, podemos jerarquizar la semántica diciendo que una semántica es la abstracción de otra si y solo si dos programas equivalentes en el último también son equivalentes en el primero. Estas relaciones han sido formalizadas por la teoría de la interpretación abstracta.

Podemos completar esta jerarquía ( orden parcial ) sobre las equivalencias semánticas, colocando la identidad en la parte superior (dos programas son idénticos si y solo si son la misma secuencia de caracteres), y en la parte inferior, la abstracción más común. bruto que se llama caos , donde cualquier programa es equivalente a cualquier otro programa.

Ediciones 2020-21

Leer también: Qué es la búsqueda semántica, definición, significadoCo-Citacion, semántica, bibliografía, SEO, qué esSimilitud semántica o proximidad, qué es; motores de búsqueda, webBúsqueda semántica, tendencias; motores de búsqueda

This post is also available in: Español