Please enable JavaScript.
Coggle requires JavaScript to display documents.
Conceitos das LPs - Coggle Diagram
Conceitos das LPs
Semântica Axiomática
A semântica axiomática define axiomas (afirmações básicas que são assumidas como verdadeiras) e regras de inferência (formas de derivar novas verdades a partir dos axiomas).
Exemplo: Se quisermos provar que um programa que ordena uma lista sempre resulta em uma lista ordenada, usamos a semântica axiomática para formalizar essa propriedade e derivar uma prova.
Importância: É fundamental para a verificação formal de programas, permitindo a derivação de provas matemáticas que garantem a correção do código em relação às especificações.
Exemplo: Um axioma básico pode ser que a atribuição x := e muda o valor de x para o valor de e, enquanto uma regra de inferência poderia determinar como a execução de um bloco de código afeta as condições de pós-execução.
Conceito: A semântica axiomática usa lógica formal para descrever o significado dos programas. Ela se baseia em axiomas e regras de inferência para estabelecer verdades sobre o comportamento de programas.
Semântica Operacional
Objetivo: Fornecer uma visão passo a passo de como um programa é executado, descrevendo o comportamento do programa em termos de estados de execução.
A avaliação de expressões na semântica operacional é feita através de uma sequência de transições entre estados. Cada transição representa a aplicação de uma operação que transforma um estado inicial em um estado final.
Definição: A semântica operacional define o significado de um programa através da descrição das operações realizadas por um interpretador ou máquina abstrata ao executar o programa. Ou seja, é uma forma de entender como as instruções de um programa alteram o estado do sistema.
Exemplo: Em uma expressão aritmética como 3 + 5, a semântica operacional descreve como essa expressão é avaliada passo a passo, começando do estado inicial (onde as variáveis e valores são definidos) até o estado final (onde o resultado da expressão é obtido).
Semântica Denotacional
Propósito: Facilitar a análise formal de programas e provar propriedades como correção e equivalência, fornecendo uma representação matemática clara do comportamento do programa.
A semântica denotacional é usada para definir funções matemáticas que modelam o comportamento de construções de linguagem de programação, como expressões, comandos e procedimentos.
Definição: A semântica denotacional associa cada parte de um programa a uma função matemática que mapeia estados iniciais a estados finais. Ela busca descrever o significado de um programa de maneira abstrata, sem focar em como a execução ocorre.
Exemplo: Para a expressão x := 2 + 3, a semântica denotacional poderia associar essa expressão a uma função que mapeia qualquer estado onde x é indefinido ou diferente de 5 para um estado onde x é 5.
-
-