Na semântica axiomática, cada instrução de um programa é associada a pré-condições e pós-condições, que são expressões lógicas que descrevem as condições antes e depois da execução da instrução. Essas condições são usadas para construir provas formais da corretude do programa.
Exemplo de Axioma: O axioma de atribuição de Hoare, {P[E/x]} x := E {P}, onde P é uma expressão lógica e x := E é uma instrução de atribuição, estabelece que se a expressão P é verdadeira antes da atribuição, então ela continuará verdadeira após a atribuição, desde que todas as ocorrências de x em P sejam substituídas por E.