La semántica en programación es una disciplina que estudia la formalización de los significados de las construcciones del lenguaje de programación mediante la construcción de sus modelos matemáticos formales . Se pueden usar varias herramientas como herramientas para construir tales modelos, por ejemplo, lógica matemática , cálculo λ , teoría de conjuntos , teoría de categorías , teoría de modelos , álgebra universal . La formalización de la semántica de un lenguaje de programación se puede utilizar tanto para describir el lenguaje, para determinar las propiedades del lenguaje, como para propósitos de verificación formal de programas en este lenguaje de programación.
La semántica de una lengua es el significado semántico de las palabras. En programación, el significado semántico inicial de los operadores , las construcciones básicas del lenguaje, etc.
Ejemplo:
Primer código: yo=0; mientras(i<5){i++;} Segundo código: yo=0; hacer{i++;} while(i<=4);Lógicamente, estos dos fragmentos de código hacen lo mismo, los resultados de su trabajo son idénticos. Al mismo tiempo, semánticamente, se trata de dos ciclos diferentes . También etiquetas:
<i></i> <em></em>se verán exactamente iguales en la página, es decir, en realidad representarán lo mismo, y semánticamente, la primera etiqueta está en cursiva y la segunda es una selección lógica (los navegadores se muestran en cursiva).
La semántica operacional se utiliza para los conceptos sintácticos del lenguaje . Trata las funciones como definiciones textuales bien formadas que brindan aplicación a un argumento, y no como funciones en el sentido matemático del término.
Existe una clasificación de diferentes tipos de semántica operacional:
Semántica axiomática : la semántica de cada construcción sintáctica en un idioma se puede definir como un conjunto de axiomas o reglas de inferencia que se pueden usar para inferir los resultados de esa construcción. Para comprender el significado de todo el programa, estos axiomas y reglas de inferencia deben usarse de la misma manera que en la demostración de teoremas matemáticos ordinarios. Suponiendo que los valores de las variables de entrada satisfagan algunas restricciones, los axiomas y las reglas de inferencia se pueden utilizar para obtener restricciones sobre los valores de otras variables después de la ejecución de cada instrucción del programa. Cuando se ejecuta el programa, obtenemos una prueba de que los resultados calculados satisfacen las restricciones necesarias sobre sus valores en relación con los valores de entrada. Es decir, se demuestra que la salida representa los valores de la función correspondiente calculada a partir de los valores de la entrada.
La semántica denotacional pone objetos matemáticos reales en correspondencia con expresiones en el programa , es decir, las expresiones denotan ( ing . para denotar — de ahí “denotacional”) sus valores [1] . Los resultados más importantes, incluso pioneros, en la construcción de la semántica denotacional se obtuvieron en los trabajos de D. Scott (Dana Scott) y K. Strachey (Christopher Strachey) a fines de la década de 1960 y principios de la de 1970 en la Universidad de Oxford [2] . Scott fue el primero en construir un modelo del cálculo λ basado en el concepto de un conjunto completo parcialmente ordenado. Para hacer esto, usó funciones que son continuas en dicho conjunto.
La semántica interpretativa es una descripción de la semántica operativa de las construcciones en términos de lenguajes de programación de bajo nivel ( lenguaje ensamblador , código de máquina ). Este método le permite identificar las secciones del programa de ejecución lenta y, a menudo, se usa en los fragmentos correspondientes de los sistemas de programación para optimizar el código del programa .
La semántica traslacional es una descripción de la semántica operativa de las construcciones en términos de lenguajes de programación de alto nivel . Usando este método, puede aprender un lenguaje similar al que ya conoce el programador.
La semántica transformacional es una descripción de la semántica operativa de las construcciones del lenguaje en términos del mismo lenguaje. La semántica transformacional es la base de la metaprogramación .
El tema de constante interés e investigación es la construcción de sistemas para probar la corrección o la corrección de los programas. Los sistemas de prueba para el caso de corrección de programas funcionales resultaron ser los más desarrollados, los cuales se remontan al sistema LCF de Robin Milner y al sistema de R. Boyer (R. Boyer) y J. Moore (J. Moore) .
La investigación actual se centra en construir sistemas basados en lógica constructiva y establecer una analogía entre programas y pruebas. Es significativo que tanto los programas como las demostraciones se consideren inmersos en un cálculo λ con tipos, que es un sistema formal de órdenes superiores. Esto asegura que solo se puedan construir programas que terminen. Uno de estos sistemas es el sistema Coq .