Semántica axiomática

Semántica axiomática es un enfoque basado en la lógica matemática para demostrar la correctitud de un algoritmo. Está estrechamente relacionado con la lógica de Hoare.La semántica axiomática define el significado de un comando dentro de un programa, mediante la descripción de su efecto sobre las aserciones acerca del estado del programa.El primer aporte significativo en esta aproximación, fue realizado por Hoare y Wirth en 1980. más precisamente para proveer la semántica del lenguaje Pascal.