Imagem de fundo

Considere o seguinte trecho de código simples: { x > 0 } y := x + 1 { y > 1 } A p...

Considere o seguinte trecho de código simples:


{ x > 0 }

y := x + 1

{ y > 1 }


A pré-condição { x > 0 } garante que, depois da execução da instrução y := x + 1, a pós-condição {y > 1} será satisfeita, permitindo raciocinar formalmente sobre a correção do programa sem executá-lo.


Com base nessa abordagem, qual é o tipo de semântica formal utilizada para relacionar pré-condições e pós-condições e raciocinar sobre a correção do programa?


A

Semântica operacional.


B

Semântica denotacional.


C

Semântica axiomática.


D

Semântica natural.


E

Semântica composicional.