Click here to load reader

Semântica em Linguagens de Programação Semântica Denotacional

  • View
    41

  • Download
    0

Embed Size (px)

DESCRIPTION

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]). Semântica Denotacional. Motivação - PowerPoint PPT Presentation

Text of Semântica em Linguagens de Programação Semântica Denotacional

  • Semntica em Linguagens de Programao

    Semntica DenotacionalParadigmas de Linguagens de ProgramaoCin/UFPE

    Fred Duro ([email protected])Kellyton Brito ([email protected])Leonardo Martins ([email protected])

  • Semntica DenotacionalMotivao

    Analisar um programa a partir somente da sintaxe da linguagem, sem necessariamente ter que execut-la;

    Aplicaes

    Provar a exatido de programas;Verificar a equivalncia semntica;Auxiliar a criao do projeto da linguagem;Criar compiladores;

  • Semntica DenotacionalHistria

    Dana Scott em 1970Lambda clculo;Funes Computacionais

    Teoria do Domnio;teoria matemtica de linguagens de programao;aproximao e convergncia de conjuntos (ponto fixo);o significado das estruturas de uma linguagem de programao;

  • Tipos de Semntica FormalSemntica OperacionalComo o programa executado? Que operaes so realizadas?

    Semntica DenotacionalO que o programa significa? Que objetos matemticos ele denota?

    Semntica AxiomticaQuais proposies lgicas so vlidas para um programa? ex.:{x = 4} x + 1 {x = 5}

  • Tipos de Semntica FormalSemntica Operacional

    Semntica Denotacional

    Semntica Axiomtica

  • Semntica DenotacionalConceito

    Estuda o significado dos programas;Mapeia construes sintticas para objetos matemticos, atravs de uma funes semntica

    Ex: C[[x := a]] = {(, [n/X]) | & n = A[[a]]}

    Para C[[x := 3]] = {(, [n/X]) | & n = A[[3]]}

    Outras estruturas sintticas que podem ser mapeadas:Comandos:Skip; While; Write; Read; If Then Else; AtribuioExpresses:Aritmticas;Boleanas;

  • Semntica DenotacionalNotaes para expressar a semntica

    NotaesInduo EstruturalA[[n]] = {(, n) | }

    Notao LambdaEx: A[[n]] = .n

  • Semntica DenotacionalDomnios Sintticos

    Aexp a ::= x | n | a1 + a2 | a1 a2 | a1 a2

    os significados de elementos de Aexp pertencem ao conjunto de funes totais IZ

    Bexp b ::= t | a1 = a2 | a1 < a2 | b | b1 ^ b2 | b1 v b2 os significados de elementos de Bexp pertencem ao conjunto de funes 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 funes

  • Semntica DenotacionalSemntica Composicional

    O significado de comandos de uma linguagem IMP deve ser uma funo pertencente ao conjunto de funes parciais -> .

    Ex1: C[[C0; C1]] = C[[c1]] o C[[c0]]

    A denotao de uma parte de um programa determinada somente pela denotao das suas subpartes (a semntica dita composicional).

    Ex2: A[[a0 + a1]] = {(,n0 + n1) | (,n0) A[[a0]] & (,n1) A[[a1]] }

  • Semntica DenotacionalEquaes Semnticas 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]] }

  • Semntica DenotacionalEquaes Semnticas 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}

  • Semntica DenotacionalEquaes Semnticas 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 BulaNext Page

  • Semntica DenotacionalEquao Semntica do WHILE Considerando que w while b do c nota- se a equivalncia:

    w ~ if b then c; w else skip

    Semntica de C[[W]] ento dada por:

    C[[w]] = {(, ) | B[[b]] = true & (, ) C[[w]] o C[[c]] } U {(, ) | B[[b]] = false }

    Considerando que C[[w]] = , nota se que: = ();

    Essa relao se aproxima do conceito de ponto fixoEquao Recursiva

  • Semntica DenotacionalPonto Fixo

    Em funo de primeira ordem:

    Um ponto fixo de uma funco 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 funes de alta ordem:

    Os argumentos agora so funces -> fix(f);Ex do Caso do While para fix(), temos: () = .

  • Semntica DenotacionalEquaes Semnticas do While

    C[[while b do c]] = fix(), onde

    () = {(, ) | B[[b]] = true & (, ) o C[[c]] } U {(, ) | B[[b]] = false }

  • Semntica DenotacionalO Projeto

    Objetivo inicial:Expressar Semntica Operacional/Denotacional da Linguagem;

    Abordagem da Equipe:Viso Operacional;FerramentaAprofundamento dos Conceitos de Semntica Denotacional;

  • Semntica DenotacionalO Projeto Abordagem Operacional

    Apresentao do comportamento do ambienteCriao da Ferramenta:Exibio da viso operacional do ambienteExibio das funes semnticas

  • Semntica DenotacionalFerramentaUtilizao de Aspectos

    Insero dos mtodos:meaning();denotational();

  • Implementao da FerramentaO Projeto Abordagem Operacional

    Apresentao do comportamento do ambienteCriao da Ferramenta:Exibio da viso operacional do ambienteExibio das funes semnticas

  • Semntica DenotacionalTrabalho Futuro - O Projeto de Fato

    1 - Traduo da sintaxe original para uma linguagem semntica

    var a = 2; -> {(, [n/X]) | & n = A[[2]] }var b = 3; -> {(, [n/X]) | & n = A[[3]] } {(, [n/X]) | & n = A[[2]] o n = A[[3]] }

    2 Criao de um interpretador para a linguagem semntica Criao do Ambiente Semntico; Etc

    3 Execuo da linguagem semntica ou Animao

  • RefernciasProgramming Language Syntax and Semantics. David A Watt. Prentice Hall, 1991. Captulo 3.;Semantics With Applications, A Formal Introduction. Hanne Nielson, Flemming Nielson;The Formal Semantics of Programming Languages, Glynn Winskel

Search related