Sem¢ntica Formal

  • View
    4.645

  • Download
    1

Embed Size (px)

DESCRIPTION

Lâminas para um curso de 1 semestre de Semântica Formal

Text of Sem¢ntica Formal

  • 1. 1 Semntica Formala Carlos A. P. Campani 22 de julho de 2005

2. 2 Copyright c 2005 Carlos A. P. Campani. E garantida a permisso para copiar, distribuir e/oua modicar este documento sob os termos da Licena de c Documentaao Livre GNU (GNU Free Documentation c License), Verso 1.2 ou qualquer verso posteriora a publicada pela Free Software Foundation; sem Seoes c Invariantes, Textos de Capa Frontal, e sem Textos de Quarta Capa. Uma cpia da licena inclu na seao o c eda c intitulada GNU Free Documentation License. veja: http://www.ic.unicamp.br/~norton/fdl.html. 3. 3 S mulau 1. Introduao c 2. Abordagens de semntica formal a 3. Linguagem exemplo While 4. Sintaxe abstrata 4. 4 5. Reviso de Prova de Teoremas a(a) Prova de Implicaaoc(b) Prova por Reduo ao Absurdoca (c) Prova por Induo ca i. Induo Sobre os Naturaiscaii. Induao Sobre o Tamanho de uma Seqnciacue iii. Induao Estruturalc 5. 5 6. Semntica de expresses ao(a) Nmeros e Numerais u(b) Descrevendo Estados (c) Expresses aritmticasoe(d) Expresses booleanas o 7. Propriedades da Semntica a(a) Variveis Livresa(b) Substituiao c 6. 6 8. Semntica Operacional a(a) Semntica Natural ai. Propriedades da Semnticaa ii. Funo Semnticacaa(b) Semntica Operacional Estruturada ai. Propriedades da Semnticaa ii. Funo Semnticacaa (c) Um Resultado de Equivalnciae 7. 7 9. Semntica Denotacional a(a) Composicionalidade(b) Ponto Fixo (c) Deniao da Semnticaca(d) Requisitos sobre o Ponto Fixo (e) Teoria de Pontos Fixos (f) Existnciae(g) Um Resultado de Equivalncia e 8. 8 10. Semntica Axiomticaa a (a) Provas Diretas de Correo de Programascai. Semntica Naturala ii. Semntica Operacional Estruturadaaiii. Semntica Denotacionala (b) Asseroes para Correao Parcialc c(c) Correao e Completude do Sistema Formal c (d) Asseroes para Correao Totalc c 9. 9 Bibliograa Nielson, H. & Nielson, F. Semantics withApplications: a formal introduction. dispon em: velhttp://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html; lminas para impresso: http: aa//www.ufpel.edu.br/~campani/semantica4.ps.gz. 10. 1 INTRODUCAO101IntroduocaSemntica formal preocupa-se em especicararigorosamente o signicado ou comportamento deprogramas, partes de hardware, etc.Sintaxe descreve as estruturas de uma linguagem;Semntica descreve o signicado destas estruturas. a 11. 1 INTRODUCAO 11A necessidade de uma semntica formal (matemtica) a apara linguagens de programaao justica-se pois: c pode revelar ambigidades na denio da linguagem uca (o que uma descrio no formal no permitiriaca aa revelar); uma base para implementaao (s e cntese), anlise ea vericaao formal.c 12. 2 ABORDAGENS 122AbordagensSemntica Operacional Signicado de uma construoa ca da linguagem especicado pela computaao que ela ec induz quando executada em uma mquina hipotticaae (interessa como o efeito da computaao produzido);c eSemntica Denotacional Signicados modelados pora objetos matemticos que representam o efeito de a executar uma estrutura (somente o efeito interessa, no como produzido);aeSemntica Axiomtica Especica propriedades doaa efeito da execuao das estruturas como asseresc co (alguns aspectos da execuao so ignorados). c a 13. 2 ABORDAGENS13Tipos de Semntica Operacional:a Semntica Operacional Estruturada (especica mais a detalhes da execuao);c Semntica Natural (simplica a notaao e esconde a c detalhes, ao tomar um passo maior). 14. 3 LINGUAGEM EXEMPLO WHILE 143Linguagem Exemplo Whilen Num x Var a Aexp b Bexp S Stm 15. 3 LINGUAGEM EXEMPLO WHILE15 a ::= n|x|a1 + a2 |a1 a2 |a1 a2 b ::= true|false|a1 = a2 |a1 a2 |b|b1 b2S ::= x:=a|skip|S1 ; S2 |if b then S1 else S2 |while b do S 16. 3 LINGUAGEM EXEMPLO WHILE16ex1: z:=x; x:=y; y:=zex2: y:=1; while (x = 1) do (y:=yx; x:=x1) 17. 4 SINTAXE ABSTRATA174Sintaxe Abstrataz:=x; x:=y; y:=zS A S bb ;S www www b0 b w8z := a S bb ; S aa bb1 aa0xx:= a y:= a y z 18. 4 SINTAXE ABSTRATA18S AS ww ; wwwS` ww8``0 `Sd ; S b y := add1~ ~~b1 b z:= ax:= azxy 19. 4 SINTAXE ABSTRATA 19Usando notaao linear: c z:=x; (x:=y; y:=z) (mais ` direita); a (z:=x; x:=y); y:=z (mais ` esquerda). a 20. 4 SINTAXE ABSTRATA20Exerccio: Construa a rvore sinttica de aay:=1; while (x = 1) do (y:=yx; x:=x1). 21. 5 REVISAO DE PROVA DE TEOREMAS215 Reviso de Prova de Teoremas a 5.1Prova de Implicao caPara provar A B, assuma A (hiptese) e deduza B.o A (hiptese) o ... ... . . . B AB 22. 5 REVISAO DE PROVA DE TEOREMAS22 ex: Provar que se um nmero inteiro divis por 6u evelento tambm o por 2. a eeSeja n Z, tal que n divis por 6:evel 1. n divis por 6 (hiptese);evelo 2. n = 6.k, onde k N; 3. n = 2.3.k; 4. n = 2.k , onde k = 3.k e k N 5. n divis por 2;evel 6. Logo, vale o enunciado. 23. 5 REVISAO DE PROVA DE TEOREMAS235.2 Prova por Reduo ao Absurdoca Para provar A, suponha A e mostre que isto resulta emuma contradiao (absurdo).cex: Provar que se um nmero somado a si mesmo resultauo nmero original, ento este nmero zero. uau eSuponha que este nmero x e que:u ex+x=xx=0 ento a2x = x x = 0Logo, 2 = 1 (absurdo). 24. 5 REVISAO DE PROVA DE TEOREMAS24 5.3 Prova por Induoca 5.3.1Induo Sobre os Naturais ca P (0)P (n) P (n + 1)nN nP (n)Base P (0);Passo P (n) P (n + 1); P (n) a hiptese indutiva;eo Ento, tenta-se provar P (n + 1); aConcluso nP (n). a 25. 5 REVISAO DE PROVA DE TEOREMAS 25ex: Provar que o quadrado de um nmero natural sempre u maior ou igual ao nmero.euBase 0 02 ;Passo Assumir n n2 . Ento:a n + 1 n2 + 1 n2 + 1 + 2n = (n + 1)2 Concluso n N n n2 . a 26. 5 REVISAO DE PROVA DE TEOREMAS 26 cio: Prove que para todo n N, 2nn.Exerc n(n+1)Exerc cio: Prove que 1 + 2 + 3 + + n =2. 27. 5 REVISAO DE PROVA DE TEOREMAS 275.3.2 Induo Sobre o Tamanho de umacaSeqncia ue1. Prove que a propriedade vale para todas asseqncias de comprimento 0 (base); ue 2. Prove que a propriedade vale para todas as outrasseqncias: Assuma que a propriedade vale para uetodas as seqncias de tamanho menor ou igual a kue(hiptese indutiva) e mostre que vale para seqnciaso uede tamanho k + 1. 28. 5 REVISAO DE PROVA DE TEOREMAS285.3.3 Induo Estruturalca Aplica-se sobre as estruturas de uma linguagem: 1. Prove que a propriedade vale para todas asestruturas atmicas (ex: P (x:=a) e P (skip)); o 2. Prove que a propriedade vale para qualquerprograma: Assuma que vale para as estruturas queformam um comando, e mostre que vale para ocomando composto (ex: P (S1 ) P (S2 ) P (S1 ; S2 )). 29. 6 SEMANTICA DE EXPRESSOES 296 Semntica de Expresses ao 6.1N meros e NumeraisuN : Num Z Se n Num ento escrevemos N [[n]], e usamos [[ e ]] paraaenfatizar que N uma funo semntica.eca a 30. 6 SEMANTICA DE EXPRESSOES 30 N [[0]] = 0 N [[1]] = 1N [[n 0]] = 2N [[n]]N [[n 1]] = 2N [[n]]+1 Observao: 0 o numeral (0 Num) e 0 o nmerocae eu(0 Z). 31. 6 SEMANTICA DE EXPRESSOES316.2Descrevendo Estados Estado representa uma associaao entre variveis e seus cavalores. State = Var Z ex: [x 5, y 7, z 0]. 32. 6 SEMANTICA DE EXPRESSOES 32 6.3Expresses aritmticasoe A : Aexp (State Z)A[[n]]s = N [[n]] A[[x]]s = s x A[[a1 + a2 ]]s = A[[a1 ]]s+A[[a2 ]]sA[[a1 a2 ]]s = A[[a1 ]]sA[[a2 ]]s A[[a1 a2 ]]s = A[[a1 ]]sA[[a2 ]]s Observao: s um estado. ca e 33. 6 SEMANTICA DE EXPRESSOES33ex: seja s x = 3: A[[x + 1]]s = A[[x]]s+A[[1]]s= (s x)+N [[1]]= 3+1= 4 Observao: na primeira linha, + dentro do [[.]] pertenceca` linguagem, + ` direita a operaao soma. 1 oaa ecenumeral (1 Num) e 1 o nmero (1 Z). eu 34. 6 SEMANTICA DE EXPRESSOES 346.4Expresses booleanaso B : Bexp (State T) T = {tt, } 35. 6 SEMANTICA DE EXPRESSOES35 B[[true]]s = tt B[[false]]s = tt se A[[a1 ]]s = A[[a2 ]]sB[[a1 = a2 ]]s = se A[[a1 ]]s = A[[a2 ]]s tt se A[[a1 ]]s A[[a2 ]]sB[[a1 a2 ]]s = se A[[a1 ]]sA[[a2 ]]s tt se B[[b]]s = B[[b]]s = se B[[b]]s = tt 36. 6 SEMANTICA DE EXPRESSOES 36 tt se B[[b ]]s = tt e B[[b ]]s = tt 1 2B[[b1 b2 ]]s = se B[[b1 ]]s = ou B[[b2 ]]s = 37. 7 PROPRIEDADES DA SEMANTICA377 Propriedades da Semntica a 7.1Variveis Livres aAs variveis livres de uma expresso a denida como o aaeconjunto de variveis que ocorrem em a. aFV(n) = FV(x) = {x} FV(a1 + a2 ) = FV(a1 ) FV(a2 ) FV(a1 a2 ) = FV(a1 ) FV(a2 ) FV(a1 a2 ) = FV(a1 ) FV(a2 ) 38. 7 PROPRIEDADES DA SEMANTICA 38Teorema 1 Sejam s e s dois estados satisfazendo ques x = s x para todo x em FV(a). Ento, A[[a]]s = A[[a]]s . aProva: (por induo sobre as expresses aritmticas)caoe 1. Base:caso n Sabemos que A[[a]]s = N [[n]] e A[[a]]s = N [[n]] e assim A[[a]]s = A[[a]]s ;caso x ns temos A[[x]]s = s x e A[[x]]s = s x e, pelao hiptese, s x = s x, j que x FV(x). Logo,oa A[[a]]s = A[[a]]s ; 39. 7 PROPRIEDADES DA SEMANTICA 39 2. Passo: (supomos que o enunciado vale para a1 e a2 )caso a1 + a2 Sabemos que A[[a1 + a2 ]]s = A[[a1 ]]s + A[[a2 ]]s e A[[a1 + a2 ]]s = A[[a1 ]]s + A[[a2 ]]s . Alm disto,e FV(a1) FV(a1 + a2 ) e FV(a2) FV(a1 + a2 ). Usando a hiptese indutiva, A[[a1 ]]s = A[[a1 ]]s e o A[[a2 ]]s = A[[a2 ]]s , e fcil ver que o enunciado e a vale para a1 + a2 ;casos a1 a2 e a1 a2 similares ao anterior. 40. 7 PROPRIEDADES DA SEMANTICA 40Exerc cio: Denir o conjunto FV(b) das variveis livres aem uma expresso booleana b. aExerccio: Provar que, dados s e s satisfazendo s x = s xpara todo x FV(b), B[[b]]s = B[[b]]s . 41. 7 PROPRIEDADES DA SEMANTICA417.2Substituioca Substituio denota a operao em que se troca cada cacaocorrncia de uma varivel y de uma expresso a por eaauma outra expresso a0 .aNotaao: a[y a0 ].c 42. 7 PROPRIEDADES DA SEMANTICA42 n[y a0 ] = n a se x = y 0 x[y a0 ] = x se x = y (a1 + a2 )[y a0 ] = (a1 [y a0 ]) + (a2 [y a0 ])(a1 a2 )[y a0 ] = (a1 [y a0 ]) (a2 [y a0 ]) (a1 a2 )[y a0 ] = (a1 [y a0 ]) (a2 [y a0 ]) 43. 7 PROPRIEDADES DA SEMANTICA43Exerccio: Prove queA[[a[y a0 ]]]s = A[[a]](s[y A[[a0 ]]s]), para todo s.Exerc cio: Dena a substituiao para expressescobooleanas. 44. 8 SEMANTICA OPERACIONAL 448Semntica Operacionala Expresses aritmticas e b