Refere-se ao significado das expressões, sentenças e unidades de programa de uma linguagem de programação. A semântica dinâmica é essencial para entender exatamente o que as construções da linguagem fazem durante a execução de um programa. Embora a sintaxe seja relativamente simples de descrever, a semântica dinâmica carece de uma notação universalmente aceita, tornando-a uma tarefa desafiadora para programadores e desenvolvedores de compiladores. A especificação precisa da semântica dinâmica pode permitir a verificação de correção dos programas sem a necessidade de testes, além de auxiliar no desenvolvimento de compiladores e na descoberta de ambiguidades em projetos de linguagem​

semântica operacional é um método utilizado para descrever o significado de um programa ou de uma sentença ao especificar os efeitos de sua execução em uma máquina abstrata. O foco está nas mudanças de estado da máquina durante a execução, onde o estado é a coleção de valores no armazenamento da máquina. O objetivo principal da semântica operacional é fornecer uma forma de compreender o comportamento de um programa observando a sequência de mudanças no estado da máquina.

Esse método pode ser usado de diferentes formas, dependendo do nível de detalhe necessário. Por exemplo, na semântica operacional natural, o interesse está no resultado final da execução de um programa completo. Já na semântica operacional estrutural, o objetivo é entender o significado de um programa examinando toda a sequência de mudanças de estado que ocorrem durante a sua execução​

Na avaliação de expressões dentro da semântica operacional, as expressões são tratadas como componentes fundamentais para muitas linguagens de programação. Para simplificar, podemos considerar expressões sem efeitos colaterais e limitadas a operadores básicos como adição e multiplicação, utilizando variáveis inteiras e literais inteiros.

A avaliação de uma expressão em semântica operacional envolve a determinação do valor resultante da expressão com base nos valores das variáveis e operadores. Esse processo é descrito formalmente em termos de estados da máquina, onde o estado reflete o valor atual das variáveis envolvidas​

A semântica denotacional é um método rigoroso para a descrição do significado de programas, baseada solidamente na teoria de funções recursivas. Seu objetivo é fornecer uma representação matemática precisa do comportamento de programas, mapeando as construções da linguagem de programação para objetos matemáticos e funções. Esses objetos e funções matemáticos modelam o significado exato das construções sintáticas correspondentes, permitindo uma análise formal do comportamento de um programa sem precisar simular sua execução passo a passo​

Um exemplo de aplicação da semântica denotacional envolve a representação de números binários como cadeias de caracteres. Nesse caso, a semântica denotacional mapeia essas representações sintáticas para seus correspondentes valores matemáticos. Outro exemplo é a descrição do significado de laços lógicos, onde o comportamento do laço é descrito recursivamente, utilizando funções matemáticas para mapear o estado das variáveis do programa após as execuções necessárias do laço

A semântica axiomática é uma abordagem baseada em lógica matemática para a especificação de semântica de programas. Ao contrário de outras abordagens, ela não define diretamente o significado de um programa, mas foca no que pode ser provado sobre o programa. Isso a torna uma das abordagens mais abstratas para a semântica de linguagens de programação.

Seu conceito central é usar axiomas e regras de inferência para provar a corretude de programas, ou seja, garantir que o programa realize a computação conforme especificado. A semântica axiomática é importante especialmente para a verificação formal de programas, permitindo provar matematicamente que um programa está correto, desde que as provas possam ser construídas.

Dentro da semântica axiomática, axiomas são sentenças lógicas assumidas como verdadeiras e servem como ponto de partida para construir provas. As regras de inferência são métodos para inferir a verdade de uma asserção com base nos valores de outras asserções. A forma geral de uma regra de inferência pode ser expressa como:

S pode ser inferida. Aqui, a parte de cima é chamada de antecedente, e a parte de baixo, de consequente.

A semântica axiomática pode ser aplicada, por exemplo, na verificação da corretude de programas. Uma prova de programa normalmente envolve associar pré-condições e pós-condições a cada sentença do programa. Por exemplo, em uma sentença de atribuição como:

{x>10}. A verificação consiste em garantir que a pré-condição mais fraca possível ainda permita alcançar a pós-condição desejada .

As diferenças fundamentais entre as três abordagens de semântica residem em seus métodos de descrição do significado dos programas. A semântica operacional descreve o comportamento dos programas em termos de execução passo a passo em uma máquina abstrata, focando nas mudanças de estado durante a execução. A semântica denotacional, por outro lado, mapeia as construções da linguagem para objetos matemáticos, oferecendo uma descrição rigorosa e abstrata do significado sem se preocupar com a execução. Já a semântica axiomática não se preocupa diretamente com a execução ou mapeamento, mas foca em provar formalmente propriedades dos programas utilizando axiomas e regras de inferência lógica, assegurando a corretude em relação a especificações dadas.

Cada abordagem de semântica possui suas vantagens e desvantagens. A semântica operacional é vantajosa por ser intuitiva e próxima da implementação, facilitando a compreensão do comportamento de programas, mas pode ser complexa para descrever linguagens completas. A semântica denotacional, embora ofereça uma base matemática rigorosa e evite ambiguidades, é complexa e de difícil compreensão para quem não tem familiaridade com conceitos matemáticos avançados. A semântica axiomática se destaca por garantir a corretude dos programas através de provas lógicas, sendo essencial para sistemas críticos; no entanto, pode ser desafiadora de aplicar a programas complexos e não descreve diretamente o comportamento dos programas, mas sim as propriedades que eles devem satisfazer.

As diferentes abordagens semânticas desempenham papéis fundamentais no design e na implementação de linguagens de programação. A semântica operacional está diretamente ligada à implementação, pois modela o comportamento das construções da linguagem em termos de uma máquina abstrata, ajudando na criação de intérpretes e na definição de como o código deve ser executado. A semântica denotacional influencia o design de linguagens ao oferecer uma maneira formal de definir o significado das construções da linguagem, o que é útil na criação de compiladores e na garantia de que diferentes implementações de uma linguagem tenham o mesmo comportamento. Por fim, a semântica axiomática é crucial para a verificação formal de programas, especialmente em linguagens usadas em sistemas críticos, onde a correção é vital. Ela orienta o design para garantir que as construções da linguagem possam ser formalmente verificadas e provadas corretas, influenciando a escolha de características da linguagem que facilitem a prova de propriedades dos programas.