Please enable JavaScript.

Coggle requires JavaScript to display documents.

SIGNIFICADO DE PROGRAMAS: SEMÂNTICA DINÂMICA - Coggle Diagram

- - - - Existem diversos problemas com o uso dessa abordagem para descrições formais completas de semântica. Primeiro, os passos individuais na execução da linguagem de máquina e as mudanças resultantes no estado da máquina são muito pequenos e numerosos. Segundo, o armazenamento de um computador real é muito grande e complexo. Existem normalmente diversos níveis de dispositivos de memória, assim como conexões para incontáveis outros computadores e dispositivos de memória por meio de redes. Dessa forma, linguagens de máquina e computadores reais não são usados para semântica operacional formal. Em vez disso, linguagens de nível intermediário e interpretadores para computadores idealizados são projetados especificamente para o processo.
        
        Existem diferentes níveis de usos para a semântica operacional. No mais alto, o interesse é no resultado final da execução de um programa completo. Isso é algumas vezes chamado de semântica operacional natural. No nível mais baixo, a semântica operacional pode ser usada para determinar o significado preciso de um programa por meio do exame da sequência completa de mudanças de estados que ocorrem quando um programa é executado. Esse uso é algumas vezes chamado de semântica operacional estrutural.
- - - - O processo de construção de uma especificação de semântica denotacional para uma linguagem de programação requer que alguém defina, para cada entidade da linguagem, tanto um objeto matemático quanto uma função que mapeie as instâncias dessa entidade de linguagem para instâncias do objeto matemático. Como os objetos são definidos rigorosamente, eles modelam o significado exato de suas entidades correspondentes. A ideia é baseada no fato de que existem maneiras rigorosas de manipular objetos matemáticos, mas não construções de linguagens de programação. A dificuldade ao usar esse método está na criação dos objetos e das funções de mapeamento. O método é chamado denotacional porque os objetos matemáticos denotam o significado de suas entidades sintáticas correspondentes.
        
        As funções de mapeamento de uma especificação semântica denotacional de uma linguagem de programação, como as funções na matemática, têm um domínio e uma imagem. O domínio é a coleção de valores que são parâmetros legítimos para a função; a imagem é a coleção de objetos para os quais os parâmetros são mapeados. Na semântica denotacional, o domínio é chamado de domínio sintático, porque são mapeadas estruturas sintáticas. A imagem é chamada de domínio semântico.
        
        A semântica denotacional está relacionada à semântica operacional, na qual as construções de linguagem de programação são traduzidas para construções mais simples, o que se torna a base para o significado da construção. Na semântica denotacional, as construções de linguagem de programação são mapeadas para objetos matemáticos – conjuntos ou funções. Entretanto, diferentemente da semântica operacional, a semântica denotacional não modela o processamento computacional passo a passo dos programas.
  - - - 2 - Semântica de Linguagens Funcionais:
        Em linguagens funcionais como Haskell ou Lisp, a semântica denotacional pode ser utilizada para descrever funções recursivas e estruturas de dados imutáveis.
        
        Uma definição recursiva de uma função fibonacci(n) pode ser mapeada para uma função matemática que descreve a série de Fibonacci. A semântica denotacional fornece uma interpretação direta, usando a definição matemática da série para descrever o comportamento da função.
        
        3 - Compiladores e Otimização de Código:
        A semântica denotacional pode ser usada para provar a correção de compiladores. Por exemplo, ela pode garantir que a transformação de código de uma linguagem de alto nível para código de máquina preserva o significado original do programa.
        
        Suponha que um compilador otimize a expressão x 2 + x 2 para 2 (x 2). Usando semântica denotacional, pode-se provar que ambas as expressões têm o mesmo significado em qualquer ambiente de execução.
      - Para uma expressão E = x + 2, a semântica denotacional mapeia E para uma função f tal que, dado um ambiente ρ (um mapeamento de variáveis para valores), f(ρ) = ρ(x) + 2. Aqui, ρ(x) representa o valor da variável x no ambiente ρ.
- - - - Na semântica axiomática, não existe um modelo do estado de uma máquina ou programa, nem um modelo de mudanças de estado que ocorrem quando o programa é executado. O significado de um programa é baseado nos relacionamentos entre variáveis e constantes de um programa, os quais são o mesmo para cada execução do programa.
        
        A semântica axiomática tem duas aplicações distintas: a verificação de programas e a especificação de semântica de programas. Esta seção foca na verificação de programas e na descrição de semântica axiomática.
        
        A semântica axiomática foi definida em conjunto com o desenvolvimento de uma abordagem para provar a corretude de programas. Tais provas de corretude, quando podem ser construídas, mostram que um programa realiza a computação descrita em sua especificação. Em uma prova, cada sentença de um programa é precedida e seguida de uma expressão lógica que especifica restrições em variáveis dos programas. Tais restrições, em vez de o estado completo de uma máquina abstrata (como na semântica operacional), são usadas para especificar o significado da sentença. A notação usada para descrever restrições – que são, na verdade, a linguagem da semântica axiomática – é o cálculo de predicados. Apesar de expressões booleanas simples serem normalmente adequadas para expressar restrições, em alguns casos elas não são.
        
        Quando a semântica axiomática é usada para especificar formalmente o significado de uma sentença, ele é definido pelo efeito da sentença em asserções sobre os dados afetados pela sentença.
  - - - Verificação de Algoritmos Simples:
        Exemplo de Atribuição:
        {x = 5} y := x + 1 {y = 6} A pré-condição x = 5 garante que y = 6 após a atribuição y := x + 1.
      - Verificação de Condicionais
        Considere um comando condicional:
        {x > 0} if x > 0 then y := x else y := -x {y > 0}
        A pré-condição x > 0 garante que y > 0 após a execução do comando.
  - - - Axioma de Atribuição:
        {P[E/x]} x := E {P}
        Onde {P[E/x]} é a pré-condição obtida substituindo todas as ocorrências da variável x por E na pós-condição P.
        Exemplo: {y = 2} x := y {x = 2}
    - - Regra de Composição
        Se {P} C1 {Q} e {Q} C2 {R}, então {P} C1; C2 {R}.
        Essa regra permite concatenar comandos sequenciais.
      - Regra de Consequência
        Se {P} C {Q}, P' -> P (P implica P') e Q -> Q', então {P'} C {Q'}.
        Permite fortalecer a pré-condição e/ou enfraquecer a pós-condição.
      - Regra de Condicional (If)
        {P ∧ B} C1 {Q} e {P ∧ ¬B} C2 {Q}
        então {P} if B then C1 else C2 {Q}.
        Descreve o comportamento de um comando condicional
      - Regra de Loop (While)
        {I ∧ B} C {I} então {I} while B do C {I ∧ ¬B}.
        Onde I é o invariante de loop, que deve ser verdadeiro antes e após cada iteração do loop.