Please enable JavaScript.
Coggle requires JavaScript to display documents.
Semântica Formal - Coggle Diagram
Semântica Formal
-
Semântica Operacional
A semântica operacional descreve o significado de um programa ao detalhar, passo a passo, como seu estado é alterado durante a execução. A ideia central é simular a computação em uma máquina abstrata, focando no "como" o resultado é obtido. Ela define um conjunto de regras de transição que especificam como cada construção da linguagem transforma o estado do programa (valores de variáveis, memória, etc.).
Foco: O processo de execução, as ações e as mudanças de estado.
Analogia: É como um manual de instruções detalhado para um montador, que explica cada parafuso a ser apertado em sequência para construir um móvel.
Exemplo: Para a expressão x = 5 + 3, a semântica operacional descreveria as etapas: (1) obter o valor 5, (2) obter o valor 3, (3) realizar a operação de soma resultando em 8, (4) atualizar o estado da memória associado a x com o valor 8.
Semântica Denotacional
A semântica denotacional aborda o significado de forma mais abstrata. Em vez de descrever os passos da execução, ela mapeia cada construção da linguagem a um objeto matemático, como funções, números ou conjuntos. O objetivo é definir "o que" um programa calcula, tratando-o como uma função matemática que transforma um estado de entrada em um estado de saída.
Foco: O resultado final ou o efeito líquido, representado por uma função matemática.
Analogia: É como a planta de um arquiteto, que descreve as propriedades e as dimensões finais do móvel, sem detalhar o processo de montagem.
Exemplo: Para a mesma expressão x = 5 + 3, a semântica denotacional a representaria como uma função que, para qualquer estado de entrada, produz um estado de saída idêntico, exceto pelo fato de que o valor associado a x agora é 8. O programa inteiro é visto como uma grande função matemática.
Semântica Axiomática
A semântica axiomática não se preocupa com a execução nem com o mapeamento matemático, mas sim com a prova de propriedades sobre o programa. Ela utiliza a lógica matemática, especificamente predicados, para descrever o que deve ser verdade antes e depois da execução de um comando. A unidade fundamental é a Tripla de Hoare: {P} C {Q}.
-
-
{Q} (Pós-condição): Uma asserção lógica que será verdadeira depois da execução de C, se P era verdadeiro antes.
-
Analogia: É como o certificado de garantia de um móvel, que atesta que "se você usar o móvel em condições normais (pré-condição), ele não irá quebrar (pós-condição)".
Exemplo: Para o comando x = x + 1, a semântica axiomática poderia usar a tripla {x = 5} x = x + 1 {x = 6} para provar que, se x era 5 antes do comando, ele será 6 depois.
-