¿Qué es “la semántica formal”?

Question

Estoy leyendo un documento muy tonta y se sigue hablando acerca de cómo Giotto define una "semántica formal".

  

Giotto tiene una semántica formal que especifica el significado de modo cambia, de la comunicación intertask y de comunicación con el entorno del programa.

Estoy en el borde, pero simplemente no puedo entender lo que quiere decir con "la semántica formal."

Answer 1

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

Es lo opuesto a semántica, que es esencialmente sólo describiendo todo en la llanura Inglés. Esto puede ser más fácil de leer y entender, pero crea la posibilidad de interpretaciones erróneas, lo que podría conducir a errores porque alguien no leyó un párrafo de la manera que la intención de leerlo.

Un lenguaje de programación puede tener ambas cosas semántica formal e informal - la semántica informales servirían entonces como una explicación "texto plano" de la semántica formal y la semántica formal sería el lugar para buscar si no está seguro de lo la explicación informal realmente medios.

Answer 2

Para ampliar la respuesta de Michael Madsen un poco, un ejemplo podría ser el comportamiento del operador ++. De manera informal, se describe el operador a través de la llanura Inglés. Por ejemplo:

  

Si x es una variable de tipo int, causas ++x x para ser incrementado 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 por hacer. En primer lugar, es necesario definir una noción de tipos. En este caso, voy a suponer que todas las variables son de tipo int. En este sencillo lenguaje, el estado actual del programa puede ser descrito por una tienda, que es un mapeo de las variables de valores. Por ejemplo, en algún punto en el programa, x podría ser igual a 42, mientras que y es igual a -5,351. La tienda puede ser utilizado como una función -. Así, por ejemplo, si el s tienda tiene la variable x con el valor de 42, entonces s(x) = 42

También se incluye en el estado actual del programa son las declaraciones restantes del programa hay que ejecutar. Nosotros podemos distribuir esto como <C, s>, donde C es el programa restante, y s es la tienda.

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

A continuación, puede definir las transiciones de un estado del programa a otro - que describir lo que sucede cuando tomamos 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 tenía originalmente más uno. Todavía hay mucho trabajo que hacer, tales como la definición de la notación que se utiliza para actualizar el almacén (que yo no he hecho para detener esta respuesta conseguir incluso más tiempo!). Por lo tanto, una instancia específica de la regla general podría ser:

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

Con suerte que le da la idea. Tenga en cuenta que esto es sólo un ejemplo de la semántica formal -. Junto con la semántica operacional, no es semántica axiomática (que a menudo utiliza la lógica de Hoare) y la semántica denotativa, y probablemente muchos más que no estoy familiarizado con

Como ya he mencionado en un comentario de otra respuesta, una ventaja de la semántica formal es que se puede utilizar para probar ciertas propiedades de su programa, por ejemplo, que haya dado por terminada. Además de mostrar su programa no presenta un mal comportamiento (tales como la no terminación), también se puede demostrar que su programa se comporta como lo requiere la prueba de su programa coincide con una especificación dada. Una vez dicho esto, nunca he encontrado la idea de la especificación y verificación de un programa único que convencer, ya que he encontrado la especificación por lo general sólo ser reescrito el programa de lógica, por lo que la especificación es la misma probabilidad de ser defectuoso.

Answer 3

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

Esta página de Una Introducción práctica a denotacional semántica es una buena introducción a cómo [denotacional] semántica se refiere a la sintaxis. El principio del libro también da una breve historia de otros enfoques, no denotacional a la semántica formal (aunque el enlace de Wikipedia Michael dio entra en más detalle, y es probablemente más arriba-hasta la fecha).

sitio del autor :

  

Modelos para la semántica no tienen   atrapado en la misma medida que el BNF   y sus descendientes tienen en la sintaxis.   Esto puede deberse a que la semántica hace   parecen ser simplemente más difícil de lo   sintaxis. El sistema es más exitoso   semántica denotacional que describe   todas las características que se encuentran en el imperativo   lenguajes de programación y tiene un sonido   base matemática. (Todavía hay   investigación activa en sistemas de tipo y   la programación en paralelo.) Muchos   definiciones denotacional pueden ser   ejecutado como intérpretes o traducido   en "compiladores", pero esto aún no ha   dirigido a los generadores de eficiencia   compiladores que puede ser otra de las razones   denotacional que la semántica es menos   popular que el BNF.

Answer 4

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

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

Un idioma especificado formalmente por el contrario se utiliza normalmente cuando es necesario hacer el razonamiento acerca de código de programa usando, por ejemplo, la comprobación de modelo o de teoremas. Idiomas que se prestan a estas técnicas tienden a ser los funcionales, tales como ML o Haskell, ya que éstas se definen mediante funciones matemáticas y transformaciones entre ellos; es decir, los fundamentos de las matemáticas.

C o C ++, por otro lado se informalmente definidos por las descripciones técnicas, si bien existen trabajos académicos que formalizan aspectos de 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 en las normas oficiales (posiblemente debido a una falta de sentido práctico, esp. dificultad para mantener).