Please enable JavaScript.
Coggle requires JavaScript to display documents.
Tipos de Semântica Formal - Coggle Diagram
Tipos de Semântica Formal
Semântica Denotacional
Definição e Propósito da Semântica Denotacional
Definição:
Método rigoroso para descrever o significado de programas.
É baseado na teoria de funções recursivas. Mapeia construções sintáticas para objetos matemáticos (objetos matemáticos denotam o significado das entidades sintáticas).
Propósito:
Fornecer uma descrição formal e precisa do significado dos programas, além de definir semântica de uma linguagem de programação de maneira matemática. Diferencia-se da semântica operacional por não modelar o processamento passo a passo, mas sim o significado final.
Componentes
Domínio Sintático:
Coleção de todas as representações sintáticas (estruturas de código).
Domínio Semântico:
Coleção de objetos matemáticos que representam o significado das estruturas sintáticas.
Exemplos de Aplicação da Semântica Denotacional
Exemplo 1: Números Binários
Sintaxe:
Cadeias de caracteres representando números binários.
Regras Gramaticais:
<bin_num> → '0' | '1' | <bin_num> '0' | <bin_num> '1'
Função Semântica Mbin
Mbin('0') = 0
Mbin('1') = 1
Mbin(<bin_num> '0') = 2 * Mbin(<bin_num>)
Mbin(<bin_num> '1') = 2 * Mbin(<bin_num>) + 1
Objetivo:
Converter cadeias binárias para números decimais.
Exemplo 2: Laços Lógicos com Pré-teste
Sintaxe:
while B do L (enquanto B for verdadeiro, execute L)
Função Semântica Ml
Verifica o valor booleano de B.
Se B é falso, retorna o estado atual.
Se B é verdadeiro, executa as sentenças L e continua iterando.
Objetivo:
Definir o comportamento de laços de repetição em termos de mudança de estado.
Semântica Operacional
Definição e Objetivo da Semântica Operacional
Definiçao:
A semântica operacional descreve o significado de uma sentença ou programa especificando os efeitos da execução em uma máquina. Ela foca em como o estado da máquina muda durante a execução do programa.
Objetivo:
Entender e descrever o significado de construções de linguagens de programação, além de fornecer uma descrição formal dos efeitos das construções no estado da máquina.
Desafios:
Complexidade da Máquina Real
Pequenos e numerosos passos na execução e
armazenamento e conexões complexas em computadores reais.
Uso de Linguagens de Baixo Nível
Linguagens de máquina são muito complexas, mas linguagens de alto nível não são adequadas para descrever semântica operacional formalmente.
Abordagem Ideal:
Deve se fazer o uso de linguagens intermediárias e interpretadores específicos. A Linguagem Intermediária deve ser clara e não ambígua e a Máquina Virtual deve ser usada para executar programas e descrever a semântica operacional natural e estrutural.
Avaliação de Expressões
Semântica Operacional Natural
: Descreve o resultado final da execução de um programa completo e foca no comportamento global e nos resultados após a execução completa.
Semântica Operacional Estrutura:
Detalha o significado através da inspeção das mudanças de estado em cada passo da execução.
Tambem examina a sequência completa de mudanças de estado resultantes da execução de um programa.
Processo Básico
Criação da Linguagem Intermediária:
Deve ser clara e adequada para a máquina virtual.
Descrição da Semântica:
Sentenças podem ser descritas em uma linguagem intermediária simples e compreensível.
Um exemplo de linguagem intermediária inclui instruções básicas como atribuições, operações aritméticas, e controle de fluxo.
Histórico e Aplicações
Vienna Definition Language (VDL)
: Usado para descrever a semântica de PL/I.
Demonstrou a eficácia e complexidade das descrições formais.
Limitações:
Complexidade das descrições pode limitar a aplicabilidade prática e dependência de linguagens de programação pode levar a circularidades.
Semântica Axional
Conceitos Principais
Asserções:
Asserções são expressões lógicas que descrevem o estado das variáveis antes (pré-condição) e depois (pós-condição) da execução de uma sentença de programa.
Pré-condição
: Restrição que deve ser verdadeira antes da execução de uma sentença.
Pós-condição
: Restrição que deve ser verdadeira após a execução da sentença.
Sentenças de Atribuição
: O axioma de atribuição define a pré-condição mais fraca para uma sentença de atribuição. Dada a sentença x = E e uma pós-condição Q, a pré-condição P é calculada como P = Q[x → E], onde todas as instâncias de x em Q são substituídas por E.
Sequências de Sentenças
:Para uma sequência de sentenças S1; S2, a pré-condição mais fraca pode ser obtida aplicando uma regra de inferência
Sentenças de Seleção (if-then-else):
A regra de inferência para a seleção requer que a pré-condição seja suficientemente forte para garantir a pós-condição tanto para o ramo then quanto para o ramo else.
Laços de Repetição (while):
A pré-condição para um laço while é determinada com o uso de uma invariante de laço. A invariante deve:
Ser verdadeira antes do início do laço (com base na pré-condição).
Permanecer verdadeira durante a execução do laço.
Garantir a pós-condição ao final do laço.
Aplicações
Verificação de Programas:
Usar asserções para provar que um programa atende às suas especificações.
Especificação Formal:
Definir precisamente o significado das sentenças de programa usando lógica matemática.
Diferenças Fundamentais
Semântica Operacional:
Descreve o comportamento de um programa em termos das operações executadas e mudanças de estado. Também detalha o passo a passo da execução.
Semântica Denotacional:
Mapeia construções de linguagem para funções matemáticas. Ela oferece uma descrição abstrata e formal do comportamento do programa.
Semântica Axiomática:
define propriedades e regras lógicas que um programa deve satisfazer. Utiliza lógica matemática para verificar a correção e segurança.
Vantagens e Desvantagens
Semântica Operacional:
Vantagens: Intuitiva para entender a execução real do programa; útil para compiladores e interpretadores. Desvantagens: Pode ser complexa para linguagens com múltiplas camadas de abstração.
Semântica Denotacional:
Vantagens: Permite uma análise formal e comparação entre linguagens; oferece uma visão matemática clara. Desvantagens: Menos intuitiva; modelagem pode ser complexa para linguagens detalhadas.
Semântica Axiomática:
Vantagens: Ideal para verificação formal; permite prova de propriedades como correção e segurança. Desvantagens: Complexa; menos focada na implementação prática.
Relação com Linguagens de Programação
Semântica Operacional:
Influencia diretamente o design de compiladores e interpretadores.
Semântica Denotacional:
Ajuda na descrição matemática e na otimização de programas; útil para análise formal.
Semântica Axiomática:
Relevante para linguagens que priorizam a segurança e a verificação formal.