Semántica de lenguajes de programación

En la Teoría de lenguajes de programación, la semántica es el campo que tiene que ver con el estudio riguroso desde un punto de vista matemático del significado de los lenguajes de programación. Esto se hace evaluando el significado de cadenas sintácticamente legales definidas por un lenguaje de programación específico, mostrando el proceso computacional involucrado. En el caso de que la evaluación fuera de cadenas sintácticamente ilegales, el resultado sería no-cómputo. La semántica describe el proceso que una computadora sigue cuando ejecuta 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 el programa se ejecutará en cierta plataforma, y consecuentemente creando un modelo de computación.

Semánticas formales ayudan, por ejemplo, a escribir compiladores, a tener un mejor entendimiento de lo que un programa está haciendo y a hacer determinadas pruebas, como demostrar que el siguiente código

tiene el mismo efecto que S1 por sí solo.

El campo de las semánticas formales abarca todo lo que sigue:

También tiene vínculos cercanos con otras áreas de la ciencia de la computación como el diseño de lenguajes de programación, teoría de tipos, intérpretes y compiladores, verificación de programas y modelos.

Hay muchos enfoques a las semánticas formales, las cuales pertenecen a tres categorías principales:

Las diferencias entre estas tres amplias clases de aproximaciones puede que a veces sean difusas, pero todas las aproximaciones conocidas a las semánticas formales usan las técnicas de arriba, o alguna combinación de ellas.

Aparte de la elección entre aproximación denotacional, operacional o axiomática, la mayoría de las variaciones en los sistemas de semántica formal vienen de la elección de la base en el formalismo matemático.

Algunas variaciones de las semánticas formales incluyen las siguientes:

Por una variedad de razones, uno pudiera querer describir las relaciones entre diferentes semánticas formales. Por ejemplo:

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

Aaby, Anthony (2004). Introducción a los lenguajes de programación. Semantics.