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 $\{P\}Q\{R\}$, $P$ e $R$ são asserções. $P$ é chamada de pré-condição, representando uma sentença que é verdadeira antes da execução do comando $Q$, e $R$ é chamada de póscondição, representando uma sentença que é verdadeira após a execução do comando $Q$.

A abordagem axiomática foi proposta por Floyd e Hoare na década de 1960.

Ver também

• Semântica formal
• Ciência da computação
• Linguagens de programação
• Linguagens formais e compiladores

Referências

• Nielson, H. & Nielson, F. Semantics with Applications: a formal introduction. disponível em: http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html
• lâminas para curso de um semestre de duração de semântica formal a nível de graduação

Leitura adicional

• C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580 and 583, October 1969.
• Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19-32, Providence, Rhode Island, 1967. American Mathematical Society.