semântica axiomática

Semântica axiomática é uma abordagem de semântica formal. A semântica formal é uma das áreas de estudo de ciência da computação, preocupada em atribuir significado às construções das linguagens de programação. Nesta abordagem se especificam propriedades do efeito da execução das estruturas como asserções, que são sentenças da lógica de predicados. Estas sentenças são usualmente chamadas de axiomas, e daí o nome desta abordagem. Como as asserções se referem aos valores das variáveis dos programas, alguns aspectos da execução são ignorados. A abordagem axiomática enfatiza a possibilidade de provar propriedades de programas usando-se lógica formal, particularmente verificação formal. A abordagem faz uso de asserções, que são sentenças da lógica definidas sobre os valores das variáveis do programa. Por exemplo, em , e são asserções. é chamada de pré-condição, representando uma sentença que é verdadeira antes da execução do comando , e é chamada de póscondição, representando uma sentença que é verdadeira após a execução do comando . A abordagem axiomática foi proposta por Floyd e Hoare na década de 1960.