Hispanopedia WikiLa semántica axiomática es un enfoque basado en la lógica matemática para demostrar la corrección de los programas informáticos . [1] Está estrechamente relacionada con la lógica de Hoare .
La semántica axiomática define el significado de un comando en un programa al describir su efecto sobre las afirmaciones acerca del estado del programa. Las afirmaciones son enunciados lógicos (predicados con variables), donde las variables definen el estado del programa.
Véase también
- Semántica algebraica (ciencia informática) —en términos de álgebras
- Semántica denotacional : mediante la traducción del programa a otro lenguaje
- Semántica operacional —en términos del estado del cómputo
- Semántica formal de los lenguajes de programación : descripción general
- Semántica del transformador de predicado : describe el significado de un fragmento de programa como la función que transforma una poscondición en la precondición necesaria para establecerla.
- Afirmación (informática)
Referencias
- ^ Winskel, Glynn (5 de febrero de 1993). La semántica formal de los lenguajes de programación: una introducción. MIT Press. ISBN 978-0-262-73103-4.