Please enable JavaScript.
Coggle requires JavaScript to display documents.
Semânticas Formais - Henrique - Coggle Diagram
Semânticas Formais - Henrique
Semântica Operacional
Definição
Descrever como os programas são executados passo a passo
Descrever o significado de uma sentença
ou programa pela especificação dos efeitos de rodá-lo em uma máquina
Definir claramente o que programas fazem, explicando o papel de cada parte da linguagem
Provar propriedades dos programas, como se estão corretos ou seguros
Orientar a criação de compiladores e interpretadores, agindo como um guia detalhado de como a linguagem deve funcionar
Objetivo
Expressões são transformadas em seus valores ou formas mais simplificadas através de regras de avaliação.
Regras de transição ou relações de avaliação, que descrevem como um estado do programa muda para outro estado
(3 + 2) * 4
3 + 2 = 5
5 * 4
20
Avaliação de expressões
Semântica Denotacional
Definição
Busca dar significado aos programas através da sua tradução para objetos matemáticos, permitindo uma descrição de alto nível do comportamento do programa
Abstrair os detalhes da execução e foca no resultado final da computação
Propósito
Fornecer uma fundação matemática para o entendimento e a análise dos programas
Abstração: Oferece uma visão de alto nível do que os programas fazem, sem se prender aos detalhes de como as operações são realizadas
Independência da Implementação: Ao focar no significado dos programas em vez de como eles são executados, facilita a portabilidade e a compreensão de diferentes paradigmas de programação
Rigor Matemático: Permite a formalização e a prova de propriedades importantes dos programas, como a equivalência de programas, correção, e outras propriedades lógicas
Exemplos de aplicação
Verificação Formal de Programas
Especificar formalmente a correção de um algoritmo de ordenação, provando que, para qualquer lista de entrada, a saída será uma lista ordenada dos elementos de entrada
Otimização de Código em Compiladores
Um compilador pode identificar que a expressão x * 0 sempre resulta em 0, independente do valor de x
Com base na semântica denotacional, o compilador pode otimizar o programa substituindo a expressão por 0, reduzindo assim o custo computacional sem alterar o resultado do programa
Comparação entre elas
Diferenças Fundamentais
Semântica Operacional: Foca em como os programas são executados em termos de passos computacionais. Descreve a execução do programa como uma sequência de passos de transição de estados
Vantagens e Desvantagens
Semântica Operacional
Mais intuitiva para programadores, pois reflete o processo de execução do programa
Útil para projetar interpretadores e compiladores
Pode ser mais complexa para sistemas grandes, devido ao detalhamento dos passos de execução
Menos adequada para provar propriedades abstratas dos programas
Semântica Denotacional
Proporciona um alto nível de abstração, permitindo a prova de propriedades de programas de forma rigorosa
Independente da máquina, facilitando a portabilidade e compreensão dos programas em diferentes plataformas
Pode ser difícil de construir para linguagens de programação complexas
Requer um sólido entendimento de conceitos matemáticos
Semântica Axiomática
Poderosa para verificação formal de programas, especialmente para provar correção e segurança
Abstrata e de alto nível, foca nas propriedades lógicas sem se prender a detalhes de implementação
Requer um profundo entendimento de lógica formal
Pode ser desafiador aplicar a sistemas reais de grande escala devido à complexidade da prova de propriedades
Semântica Denotacional: Usa funções matemáticas para mapear programas a seus significados, focando nos resultados finais da execução ao invés de como os resultados são alcançados.
Semântica Axiomática: Baseia-se em axiomas e regras de inferência para provar propriedades dos programas, como sua correção. Não se preocupa diretamente com a execução do programa, mas com a verificação de suas propriedades lógicas
Concentrar no processo de execução dos programas (Semântica Operacional)
Concentrar no resultado final das computações (Semântica Denotacional)
Concentrar na verificação da correção dos programas através de proposições lógicas (Semântica Axiomática)
Semântica Axiomática
ou
Lógica de Hoare
Definição
Utiliza axiomas e regras de inferência para descrever e provar propriedades dos programas
Foca na verificação da correção dos programas através de proposições lógicas
Importância
Capacidade de prover uma metodologia formal para a verificação de correção de programas
Permite aos desenvolvedores afirmar e provar que, se um programa é iniciado em um estado que satisfaz a pré-condição P, e o programa é executado corretamente, então o estado final satisfará a pós-condição Q
Axiomas
São afirmações ou proposições que são assumidas como verdadeiras dentro de um determinado sistema formal
Servem como a base para definir o comportamento fundamental das operações mais simples em linguagens de programação
Adição de dois números
Atribuição de um valor a uma variável
Sem necessidade de prova, pois são considerados evidentemente verdadeiros dentro do contexto da linguagem de programação
Regras de Inferência
Princípios usados para derivar novas afirmações verdadeiras a partir de afirmações já estabelecidas
Permitem que desenvolvedores deduzam a correção de blocos de código mais complexos, baseando-se nos axiomas e em afirmações previamente provadas
Regra da composição
Permite inferir a correção de duas instruções sequenciais no programa se a correção de cada uma individualmente for conhecida
Exemplos de uso
Verificação da correção de um loop
Invariante de Loop: Uma propriedade que deve ser verdadeira antes e depois de cada iteração do loop. No caso, uma possível invariante é que "total é a soma de todos os números de 1 até i-1"
Usamos axiomas para definir a correção das operações básicas (como a atribuição)
Regras de inferência para deduzir a correção do loop inteiro baseado no invariante.
Relação com Linguagens de Programação
Semântica Operacional
No design de uma linguagem de programação, a semântica operacional pode ajudar a definir a execução precisa das construções da linguagem
No design da linguagem x, podemos definir a semântica operacional das construções básicas da linguagem, como atribuições e operações aritméticas
Podemos especificar que uma atribuição x = y + z em linguagem x significa que o valor de y é adicionado ao valor de z e o resultado é armazenado na variável x
Na implementação, a semântica operacional pode ser utilizada para desenvolver um interpretador ou compilador que simule a execução do programa em um modelo de máquina específico
Na implementação de x, podemos desenvolver um interpretador que simule a execução do programa em um modelo de máquina específico, seguindo as regras definidas pela semântica operacional
Obter os valores de y e z
Adicionar os valores de y e z
Armazenar o resultado na variável x
Semântica Denotacional
No design de uma linguagem de programação, a semântica denotacional pode ajudar a garantir uma especificação precisa do comportamento da linguagem
Para o design da linguagem x, podemos definir a semântica denotacional das operações de adição e multiplicação como funções matemáticas
Semântica denotacional da adição como a função matemática que recebe dois números como entrada e retorna sua soma
Na implementação, a semântica denotacional pode ser usada para criar um interpretador ou compilador que traduza as construções da linguagem para funções matemáticas correspondentes
Podemos criar um interpretador que traduza as construções da linguagem em funções matemáticas correspondentes
Para a operação de adição, o interpretador pode reconhecer a expressão de adição na linguagem x e traduzi-la em uma chamada para a função de adição definida na semântica denotacional
a = 3 + 4
O interpretador x traduziria a expressão 3 + 4 em uma chamada para a função de adição denotacional
Semântica Axiomática
No design de uma linguagem de programação, a semântica axiomática pode ser usada para especificar propriedades que devem ser mantidas durante a execução do programa
No design da linguagem x, podemos especificar propriedades que devem ser mantidas durante a execução do programa, utilizando axiomas
Podemos definir axiomas que estabelecem propriedades matemáticas básicas, como a comutatividade da adição ou a distributividade da multiplicação
Na implementação, a semântica axiomática pode ser útil para verificar a correção de programas e otimizar o código para garantir que as propriedades especificadas sejam atendidas.
Ao otimizar o código que envolve operações aritméticas, podemos aplicar regras baseadas nos axiomas para simplificar expressões e melhorar o desempenho
Os axiomas podem ser usados para verificar automaticamente a correção do programa, garantindo que as propriedades especificadas pelos axiomas sejam mantidas durante a execução
x = 2 * (3 + 4)
a
(b + c) = (a
b) + (a * c)
2
(3 + 4) = (2
3) + (2 * 4) = 6 + 8 = 14
x = 2 * (3 + 4) para 14
