¿Qué es "semántica formal"?

Question

Estoy leyendo un papel muy tonto y sigue hablando de cómo Giotto define una "semántica formal".

Giotto tiene una semántica formal que especifica el significado de los conmutadores de modo, de comunicación interna y de comunicación con el entorno del programa.

Estoy al borde de, pero simplemente no puedo captar lo que significa "semántica formal".

Answer 1

Formal semantics describen la semántica en - bien, de una manera formal - usando notación que expresa el significado de las cosas de una manera no ambigua.

Es lo contrario de semántica informal, que básicamente se trata de describir todo en inglés sencillo. Esto puede ser más fácil de leer y entender, pero crea la posibilidad de interpretaciones erróneas, lo que podría provocar errores porque alguien no leyó un párrafo de la forma en que usted quería que lo leyeran.

Un lenguaje de programación puede tener tanto semántica formal como informal: la semántica informal serviría entonces como una explicación de "texto sin formato" de la semántica formal, y la semántica formal sería el lugar para mirar si no está seguro qué significa realmente la explicación informal.

Answer 2

Para ampliar un poco la respuesta de Michael Madsen, un ejemplo podría ser el comportamiento del operador ++. Informalmente, describimos al operador usando un inglés simple. Por ejemplo:

Si x es una variable de tipo int, ++x causas x que se incrementa en uno.

(estoy suponiendo que no haya desbordamientos de enteros, y que ++x no devuelve nada)

En una semántica formal (y voy a utilizar semántica operacional), tendríamos un poco de trabajo para hacer. En primer lugar, necesitamos definir una noción de tipos. En este caso, supondré que todas las variables son del tipo int. En este lenguaje simple, el estado actual del programa puede ser descrito por una tienda, que es un mapeo de variables a valores. Por ejemplo, en algún punto del programa, x podría ser igual a 42, mientras que y es igual a -5351. La tienda se puede usar como una función, por ejemplo, si la tienda s tiene la variable x con el valor 42, entonces s(x) = 42.

También se incluyen en el estado actual del programa las declaraciones restantes del programa que tenemos que ejecutar. Podemos agrupar esto como <C, s>, donde C es el programa restante, y s es la tienda.

Por lo tanto, si tenemos el estado <++x, {x -> 42, y -> -5351}>, esto es informalmente un estado donde el comando único que queda es para ejecutar ++x, la variable x tiene un valor de 42, y la variable tiene un valor y-5351.

Podemos entonces definir transiciones de un estado del programa a otro - describimos lo que ocurre cuando damos el siguiente paso en el programa.Así, por ++, podríamos definir la semántica siguiente:

<++x, s> --> <skip, s{x -> (s(x) + 1)> 

Un tanto de manera informal, mediante la ejecución de ++x, el siguiente comando es skip, que no tiene ningún efecto, y las variables de la tienda son sin cambios, excepto por x, que ahora tiene el valor que originalmente tenía más uno. Todavía queda algo por hacer, como definir la notación que utilicé para actualizar la tienda (¡lo cual no he hecho para evitar que esta respuesta se prolongue aún más!). Por lo tanto, una instancia específica de la regla general podría ser:

<++x, {x -> 42, y -> -5351}> --> <skip, {x -> 43, y -> -5351}> 

Espero que eso le dé la idea. Tenga en cuenta que este es solo un ejemplo de semántica formal: junto con la semántica operacional, existe una semántica axiomática (que a menudo utiliza la lógica de Hoare) y una semántica denotacional, y probablemente mucho más con lo que no estoy familiarizado.

Como mencioné en un comentario a otra respuesta, una ventaja de la semántica formal es que puede usarlos para probar ciertas propiedades de su programa, por ejemplo, que termina. Además de mostrar que su programa no exhibe un mal comportamiento (como la no terminación), también puede probar que su programa se comporta según lo requerido demostrando que su programa coincide con una especificación dada. Habiendo dicho eso, nunca he encontrado la idea de especificar y verificar un programa tan convincente, ya que he encontrado que la especificación generalmente es solo el programa reescrito en lógica, por lo que la especificación es muy probable que tenga fallas.

Answer 3

Al igual que la sintaxis de un lenguaje puede describirse mediante una gramática formal (por ejemplo, BNF), es posible utilizar diferentes tipos de formalismos para asignar esa sintaxis a objetos matemáticos (es decir, el significado de la sintaxis).

This page de A Practical Introduction to Denotational Semantics es una buena introducción a cómo la semántica [denotacional] se relaciona con la sintaxis. El comienzo del libro también ofrece una breve historia de otros enfoques no denotacionales a la semántica formal (aunque el enlace de wikipedia Michael dio más detalles, y probablemente esté más actualizado).

De the author's site:

Modelos para la semántica no han atrapado en la misma medida que el BNF y sus descendientes tienen en la sintaxis. Esto puede deberse a que la semántica does parece ser simplemente más difícil que la sintaxis . El sistema más exitoso es la semántica denotativa que describe todas las características que se encuentran en los lenguajes de programación imperativa y tiene una base matemática de sonido . (Todavía hay investigación activa en los sistemas de tipo y programación paralela.) Muchos definiciones denotacional pueden ser ejecutados como intérpretes o traducidos en "compiladores" pero esto aún no ha llevó a generadores de eficientes compiladores que puede ser otro razón que la semántica denotational es menos popular que BNF .

Answer 4

¿Qué se entiende en el contexto de un lenguaje de programación como Giotto es, que una lengua con la semántica formal, tiene una matemáticamente rigurosa interpretaciónde sus construcciones de lenguaje individuales.

La mayoría de los lenguajes de programación actuales no están rigurosamente definidos. Pueden adherirse a documentos estándar que son bastante detallados, pero en última instancia es responsabilidad del compilador emitir código que de alguna manera se adhiere a esos documentos estándar.

Por otro lado, un lenguaje formalmente especificado se usa normalmente cuando es necesario razonar acerca del código de programa utilizando, por ejemplo, comprobación de modelo o demostración de teorema. Los lenguajes que se prestan a estas técnicas tienden a ser funcionales, como ML o Haskell, ya que estos se definen usando funciones matemáticas y transformaciones entre ellos; es decir, los fundamentos de las matemáticas.

C o C++ por otro lado se definen informalmente por descripciones técnicas, aunque existen documentos académicos que formalizan aspectos de estos idiomas (por ejemplo, Michael Norrish: una semántica formal para C++, https://publications.csiro.au/rpr/pub?pid=nicta:1203), pero que a menudo no encuentran su camino hacia los estándares oficiales (posiblemente debido a la falta de practicidad, especialmente la dificultad de mantener).