stringtranslate.com

Semántica (informática)

En la teoría de los lenguajes de programación , la semántica es el estudio matemático riguroso del significado de los lenguajes de programación . [1] La semántica asigna un significado computacional a cadenas válidas en la sintaxis de un lenguaje de programación . Está estrechamente relacionada con la semántica de las demostraciones matemáticas y a menudo se cruza con ella .

La semántica describe los procesos que sigue una computadora al ejecutar un programa en ese lenguaje específico. Esto se puede hacer describiendo la relación entre la entrada y la salida de un programa, o dando una explicación de cómo se ejecutará el programa en una determinada plataforma , creando así un modelo de computación .

Historia

En 1967, Robert W. Floyd publicó el artículo Asignación de significados a los programas ; su principal objetivo era "un estándar riguroso para las pruebas sobre programas informáticos, incluidas las pruebas de corrección , equivalencia y terminación". [2] [3] Floyd escribió además: [2]

En nuestro enfoque, una definición semántica de un lenguaje de programación se basa en una definición sintáctica . Debe especificar cuáles de las frases de un programa sintácticamente correcto representan comandos y qué condiciones deben imponerse a una interpretación en las proximidades de cada comando.

En 1969, Tony Hoare publicó un artículo sobre la lógica de Hoare basada en las ideas de Floyd, ahora a veces llamadas colectivamente semántica axiomática . [4] [5]

En la década de 1970 surgieron los términos semántica operacional y semántica denotacional . [5]

Descripción general

El campo de la semántica formal abarca todo lo siguiente:

Tiene estrechos vínculos con otras áreas de la informática , como el diseño de lenguajes de programación , la teoría de tipos , los compiladores e intérpretes , la verificación de programas y la comprobación de modelos .

Aproches

Existen muchos enfoques de la semántica formal; estos pertenecen a tres clases principales:

Aparte de la elección entre enfoques denotacionales, operacionales o axiomáticos, la mayoría de las variaciones en los sistemas semánticos formales surgen de la elección del formalismo matemático de apoyo. [ cita requerida ]

Variaciones

Algunas variaciones de la semántica formal incluyen las siguientes:

Describiendo relaciones

Por diversas razones, es posible que se desee describir las relaciones entre diferentes semánticas formales. Por ejemplo:

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

Véase también

Referencias

  1. ^ Goguen, Joseph A. (1975). "Semántica de la computación". Teoría de categorías aplicada a la computación y el control . Apuntes de clase sobre informática. Vol. 25. Springer . Págs. 151-163. doi :10.1007/3-540-07142-3_75. ISBN. 978-3-540-07142-6.
  2. ^ ab Floyd, Robert W. (1967). "Asignación de significados a los programas" (PDF) . En Schwartz, JT (ed.). Aspectos matemáticos de la informática. Actas del Simposio sobre matemáticas aplicadas. Vol. 19. Sociedad Matemática Americana. págs. 19–32. ISBN 0821867288.
  3. ^ Knuth, Donald E. "Resolución conmemorativa: Robert W. Floyd (1936–2001)" (PDF) . Memoriales de la facultad de la Universidad de Stanford . Sociedad Histórica de Stanford.
  4. ^ Hoare, CAR (octubre de 1969). "Una base axiomática para la programación informática". Comunicaciones de la ACM . 12 (10): 576–580. doi : 10.1145/363235.363259 . S2CID  207726175.
  5. ^ ab Winskel, Glynn (1993). La semántica formal de los lenguajes de programación: una introducción. Cambridge, Mass.: MIT Press. p. xv. ISBN 978-0-262-23169-5.
  6. ^ Schmidt, David A. (1986). Semántica denotacional: una metodología para el desarrollo del lenguaje . William C. Brown Publishers. ISBN 9780205104505.
  7. ^ Plotkin, Gordon D. (1981). Un enfoque estructural de la semántica operacional (Informe). Informe técnico DAIMI FN-19. Departamento de Ciencias de la Computación, Universidad de Aarhus .
  8. ^ ab Goguen, Joseph A. ; Thatcher, James W.; Wagner, Eric G.; Wright, Jesse B. (1977). "Semántica del álgebra inicial y álgebras continuas". Revista de la ACM . 24 (1): 68–95. doi : 10.1145/321992.321997 . S2CID  11060837.
  9. ^ Mosses, Peter D. (1996). Teoría y práctica de la semántica de la acción (informe). Informe BRICS RS9653. Universidad de Aarhus .
  10. ^ Deransart, Pierre; Jourdan, Martin; Lorho, Bernard (1988). "Gramáticas de atributos: definiciones, sistemas y bibliografía" . Apuntes de clase sobre informática 323. Springer-Verlag . ISBN. 9780387500560.
  11. ^ Lawvere, F. William (1963). "Semántica funcional de las teorías algebraicas". Actas de la Academia Nacional de Ciencias de los Estados Unidos de América . 50 (5): 869–872. Bibcode :1963PNAS...50..869L. doi : 10.1073/pnas.50.5.869 . PMC 221940 . PMID  16591125. 
  12. ^ Andrzej Tarlecki; Rod M. Burstall ; Joseph A. Goguen (1991). "Algunas herramientas algebraicas fundamentales para la semántica de la computación: Parte 3. Categorías indexadas". Ciencias de la computación teórica . 91 (2): 239–264. doi : 10.1016/0304-3975(91)90085-G .
  13. ^ Batty, Mark; Memarian, Kayvan; Nienhuis, Kyndylan; Pichon-Pharabod, Jean; Sewell, Peter (2015). "El problema de la semántica de concurrencia de lenguajes de programación" (PDF) . Actas del Simposio Europeo sobre Lenguajes y Sistemas de Programación . Springer . págs. 283–307. doi : 10.1007/978-3-662-46669-8_12 .
  14. ^ Abramsky, Samson (2009). "Semántica de la interacción: una introducción a la semántica de juegos". En Andrew M. Pitts; P. Dybjer (eds.). Semántica y lógica de la computación. Cambridge University Press. págs. 1–32. doi :10.1017/CBO9780511526619.002. ISBN 9780521580571.
  15. ^ Dijkstra, Edsger W. (1975). "Órdenes protegidas, no determinación y derivación formal de programas". Comunicaciones de la ACM . 18 (8): 453–457. doi : 10.1145/360933.360975 . S2CID  1679242.

Lectura adicional

Libros de texto
Notas de la conferencia

Enlaces externos