Semântica em Linguagens de
Programação
Semântica Denotacional
Paradigmas de Linguagens de Programação
Cin/UFPE
Fred Durão ([email protected])
Kellyton Brito ([email protected])
Leonardo Martins ([email protected])
1
Semântica Denotacional

Motivação


Analisar um programa a partir somente da sintaxe da linguagem,
sem necessariamente ter que executá-la;
Aplicações




Provar a exatidão de programas;
Verificar a equivalência semântica;
Auxiliar a criação do projeto da linguagem;
Criar compiladores;
2
Semântica Denotacional

História

Dana Scott em 1970
 Lambda cálculo;


Funções Computacionais
Teoria do Domínio;

teoria matemática de linguagens de programação;


aproximação e convergência de conjuntos (ponto fixo);
o significado das estruturas de uma linguagem de programação;
3
Tipos de Semântica Formal

Semântica Operacional


Semântica Denotacional


Como o programa é executado? Que operações são realizadas?
O que o programa significa? Que objetos matemáticos ele denota?
Semântica Axiomática

Quais proposições lógicas são válidas para um programa?
ex.:{x = 4} x + 1 {x = 5}
4
Tipos de Semântica Formal

Semântica Operacional

Semântica Denotacional

Semântica Axiomática
5
Semântica Denotacional

Conceito


Estuda o significado dos programas;
Mapeia construções sintáticas para objetos matemáticos, através de uma funções semântica
Ex: C[[x := a]] = {(σ, σ [n/X]) | σ Є Σ & n = A[[a]]σ}
Para C[[x := 3]] = {(σ, σ [n/X]) | σ Є Σ & n = A[[3]]σ}

Outras estruturas sintáticas que podem ser mapeadas :
 Comandos:


Skip; While; Write; Read; If Then Else; Atribuição
Expressões:


Aritméticas;
Boleanas;
6
Semântica Denotacional

Notações para expressar a semântica

Notações

Indução Estrutural


A[[n]] = {(σ, n) | σ Є Σ}
Notação Lambda

Ex: A[[n]] = λσ Є Σ.n
7
Semântica Denotacional

Domínios Sintáticos

Aexp a ::= x | n | a1 + a2 | a1 − a2 | a1 ∗ a2


Bexp b ::= t | a1 = a2 | a1 < a2 | ¬b | b1 ^ b2 | b1 v b2


os significados de elementos de Aexp pertencem ao conjunto de funções totais
Σ → IZ
os significados de elementos de Bexp pertencem ao conjunto de funções totais
Σ → IB
Com c ::= skip | x := n | C1; C2 | if b then C1 else C2 | while b do C

os significados de elementos de Com pertencem ao conjunto de funções
Σ→Σ
8
Semântica Denotacional

Semântica Composicional

O significado de comandos de uma linguagem IMP deve ser uma função
pertencente ao conjunto de funções parciais Σ -> Σ.


Ex1: C[[C0; C1]] = C[[c1]] o C[[c0]]
A denotação de uma parte de um programa é determinada somente pela
denotação das suas subpartes (a semântica é dita composicional).

Ex2: A[[a0 + a1]] = {(σ,n0 + n1) | (σ,n0) Є A[[a0]] & (σ,n1) Є A[[a1]] }
9
Semântica Denotacional

Equações Semânticas para Aexp

A[[n]] = {(σ, n) | σ Є Σ}

A[[X]] = {(σ, σ (X)) | σ Є Σ}

A[[a0 + a1]] = {(σ,n0 + n1) | (σ,n0) Є A[[a0]] & (σ,n1) Є A[[a1]] }

A[[a0 - a1]] = {(σ,n0 - n1) | (σ,n0) Є A[[a0]] & (σ,n1) Є A[[a1]] }

A[[a0 * a1]] = {(σ,n0 * n1) | (σ,n0) Є A[[a0]] & (σ,n1) Є A[[a1]] }
10
Semântica Denotacional

Equações Semânticas para Bexp

B[[true]] = {(σ, true) | σ Є Σ}

B[[false]] = {(σ, false) | σ Є Σ}

B[[a0 = a1]] = A[[a0]] σ = z A[[a1]] σ

B[[a0 ≤ a1]] = A[[a0]] σ ≤ z A[[a1]] σ

B[[a0 ^ a1]] = A[[a0]] σ ^ T A[[a1]] σ

B[[a0 v a1]] = A[[a0]] σ v T A[[a1]] σ

B[[¬b]] = ¬T B[[b]] σ
onde T = {true, false}
11
Semântica Denotacional

Equações Semânticas para Com

C[[skip]] = {(σ, σ) | σ Є Σ}

C[[x := a]] = {(σ, σ[n/X]) | σ Є Σ & n = A[[a]] σ}

C[[c0; c1]] = C[[c1]] o C[[c0]]

C[[if b then c0 else c1]] = {(σ, σ’) | B[[b]] σ = true & (σ, σ’) Є C[[c0]] }
U (σ, σ’) | B[[b]] σ = false &(σ, σ’) Є C[[c1]] }

C[[while b do c]] = . . . Essa aqui é pau visse..! Vide Bula…Next Page
12
Semântica Denotacional

Equação Semântica do WHILE

Considerando que w ≡ while b do c nota- se a equivalência:


w ~ if b then c; w else skip
Semântica de C[[W]] então é dada por:

C[[w]] = {(σ, σ’) | B[[b]] σ = true & (σ, σ’) Є C[[w]] o C[[c]] } U
{(σ, σ’) | B[[b]] σ = false }

Considerando que C[[w]] = φ, nota – se que:
φ = Γ(φ);
Equação
Recursiva
Essa relação é se aproxima do conceito de ponto fixo
13
Semântica Denotacional

Ponto Fixo

Em função de primeira ordem:



Um ponto fixo de uma funcão é qualquer valor x para que f(x) = x;
Ex: F(x) = x2 Pontos Fixos = {0,1} pois (0)2 = 0 e (1) 2 = 1;
Em funções de alta ordem:


Os argumentos agora são funcões -> fix(f);
Ex do Caso do While para fix(Γ), temos: Γ(φ) = φ.
14
Semântica Denotacional

Equações Semânticas do While

C[[while b do c]] = fix(Γ), onde

Γ(φ) = {(σ, σ’) | B[[b]] σ = true & (σ, σ’) Є φ o C[[c]] } U
{(σ, σ’) | B[[b]] σ = false }
15
Semântica Denotacional

O Projeto

Objetivo inicial:


Expressar Semântica Operacional/Denotacional da
Linguagem;
Abordagem da Equipe:

Visão Operacional;


Ferramenta
Aprofundamento dos Conceitos de Semântica
Denotacional;
16
Semântica Denotacional

O Projeto – Abordagem Operacional


Apresentação do comportamento do ambiente
Criação da Ferramenta:
Exibição da visão operacional do ambiente
 Exibição das funções semânticas

17
Semântica Denotacional

Ferramenta

Utilização de Aspectos

Inserção dos métodos:
meaning();
 denotational();

18
Implementação da Ferramenta

O Projeto – Abordagem Operacional


Apresentação do comportamento do ambiente
Criação da Ferramenta:
Exibição da visão operacional do ambiente
 Exibição das funções semânticas

19
20
Semântica Denotacional

Trabalho Futuro - O Projeto de Fato
1 - Tradução da sintaxe original para uma linguagem semântica
var a = 2; ->
var b = 3; ->
{(σ, σ [n/X]) | σ Є Σ & n = A[[2]] σ}
{(σ, σ [n/X]) | σ Є Σ & n = A[[3]] σ}
{(σ, σ [n/X]) | σ Є Σ & n = A[[2]] o n = A[[3]] σ}
2 – Criação de um interpretador para a linguagem semântica
•
Criação do Ambiente Semântico;
•
Etc…
3 – Execução da linguagem semântica ou Animação
21
Referências

Programming Language Syntax and Semantics. David A Watt. Prentice Hall,
1991. Capítulo 3.;


Semantics With Applications, A Formal Introduction. Hanne Nielson, Flemming
Nielson;
The Formal Semantics of Programming Languages, Glynn Winskel
22