Semântica Operacional
Semantics with Applications - A Formal Introduction
H. R. Nielson and F. Nielson
Wiley Professional Computing
Capítulo 2
DI
UFPE
Semântica Operacional

Características principais
 Significado
dos programas é especificado pela
computação que ele induz quando executado
 Preocupação
executados
DI
UFPE
com COMO os programas são
Abordagens

Semântica natural


Resultados finais
Semântica operacional estrutural
 Passos
DI
UFPE
individuais
Sistema de Transição

Componentes
 Configurações

 S,s - comando S executado no estado s

s - um estado terminal
 Relação

DI
UFPE
de transição
Diferentes abordagens: diferentes formas de
especificar a relação de transição
Semântica Natural


Transição
 Relação entre o estado inicial e o estado final
  S,s  s’
Regras
 premissas
 condições
 axiomas
 c1, e1   e1’
...  cn, en   en’

DI
UFPE
c, e   e’
if ...
Semântica Natural de While
 x := a, e   e [x |->A [[a]] e]
(atr)
 skip, s   s
(skip)
 c1, e   e’
 c2, e’   e’’
 c1 ; c2, e   e’’
 c1,e   e’
 if b then c1 else c2, e   e’
 c2, e   e’
 if b then c1 else c2, e   e’
DI
UFPE
(comp)
if B [[b]] e = true
(if-true)
if B [[b]] e = false
(if-false)
Semântica Natural de While (cont.)
 c,e   e’  while b do c, e’   e’’
 while b do c, e   e’’
 while b do c, e   e
DI
UFPE
if B[[b]] e = true (while-true)
if B[[b]] e = false
(while-false)
Árvores de Derivação

Uso das definições para derivar uma transição
 Raiz
 Nós
internos

Todas as condições devem ser satisfeitas

Tipos de árvores
 Simples:
instância de axioma
 Composta
DI
UFPE
Propriedades de uma Semântica Natural

Programas S1 e S2 são semanticamente equivalentes se
para todos os estados s e s’
 S1,s  s’ se e somente se  S2,s  s’

DI
UFPE
Árvores de derivação são a base para a prova
Propriedades de uma Semântica Natural

Semântica natural determinística
Para cada comando S e cada estado inicial s, o estado
final pode ser determinado unicamente.
Para todo comando S, e estados s, s´ e s´´
 S,s  s´ e  S,s  s´´ implica que s´ = s´´
DI
UFPE
Indução Sobre a
Forma das Árvores de Derivação

Caso base: árvores simples
 Prova

propriedades para axiomas
Passo de indução: árvores compostas
 Prova
para cada regra, assumindo válido para as
premissas

DI
UFPE
Indução estrutural nem sempre é possível
Função Semântica
Sns = Stm  (State  State)
Sns[[ S ]] s = s’ if  S,s  s’
Sns[[ S ]] s = undef, otherwise.
DI
UFPE
Semântica Operacional Estrutural

Ênfase nos passos individuais da execução

Relação de transição



DI
UFPE
S,s  
pode ter duas formas:

 S’,s’

s’
 S,s está travado se não há  tal que  S,s  
Semântica Operacional Estrutural de
While
 x := a,s  s[x  A[[a]] s ]
 skip,s  s
 S1,s   S1’,s’
 S1; S2,s   S1’; S2,s’
 S1,s  s’
 S1; S2,s   S2,s’
DI
UFPE
Semântica Operacional Estrutural de
While
 if b then S1 else S2,s   S1,s if B[[b]] s = tt
 if b then S1 else S2,s   S2,s if B[[b]] s = ff
 while b do S,s 
 if b then (S; while b do S) else skip,s
DI
UFPE
Sequência de Derivação

Sequência de configurações

S,s , 1, ... , k
 i  i + 1

DI
UFPE
 k
é travada ou terminal OU
a
sequência é infinita
Para cada passo há uma árvore de derivação
Propriedades de uma Semântica
Operacional Estrutural

Execução de um comando S em um estado s
 Termina:
 Entra

DI
UFPE
sequência de derivação finita
em “loop”: sequência de derivação infinita
Indução no comprimento das sequências de derivação
Semântica Operacional
Determinística

Para todo comando S, e estados s, s´ e s´´
 S,s   e  S,s   ´ implica que  =  ´

Há apenas uma sequência de derivação começando de
uma configuração  S,s
DI
UFPE
Equivalência de Programas

Programas S1 e S2 são semanticamente equivalentes se
para todos os estados s
  S1,s
*  se e somente se  S2,s *  , se  for
uma configuração travada ou terminal
 Há
uma sequência de derivação infinita começando
em  S1,s se e somente se há uma começando em
 S2,s
DI
UFPE
Função Semântica
Ssos = Stm  (State  State)
Ssos[[ S ]] s = s’ if  S,s * s’
Ssos[[ S ]] s = undef, otherwise.

DI
UFPE
As definições de While são equivalentes
Extensões de While
Abort

Regras anteriores não são modificadas

Nenhuma regra é adicionada

Semântica operacional estrutural
abort é diferente de skip e while true do skip

Semântica natural
abort é equivalente a while true do skip
DI
UFPE
Extensões de While
Abort

Semântica natural não distingue não-terminação de
terminação anormal

Em semântica operacional estrutural
 Não-terminação:
 Terminação
DI
UFPE
sequência de derivação infinita
anormal: configuração travada
Extensões de While
Não-determinismo

S1 or S2
 Semântica
natural
 S1,s  s’
 S1 or S2 ,s  s’
 S2,s  s’
 S1 or S2 ,s  s’
DI
UFPE
Extensões de While
Não-determinismo

Semântica operacional estrutural
 S1 or S2,s   S1,s
 S1 or S2,s   S2,s

Considere  while true do skip or x := 1
 Em
semântica natural, não-determinismo suprimirá
não-terminação, se possível
 Em
semântica operacional estrutural, isso não
acontece.
DI
UFPE
Extensões de While
Paralelismo


S1 par S2
Semântica operacional estrutural
 S1,s   S1’,s’
DI
UFPE
 S1,s  s’
 S1 par S2,s   S1’ par S2,s’
 S1 par S2,s   S2,s’
 S2,s   S2’,s’
 S2,s  s’
 S1 par S2,s   S1 par S2’,s’
 S1 par S2,s   S1,s’
Extensões de While
Paralelismo

Semântica natural
 S1,s  s’ ,  S2,s’  s”
 S1 par S2 ,s  s”
 S2,s  s’ ,  S1,s’  s”
 S1 par S2 ,s  s”
DI
UFPE
Extensões de While
Paralelismo

Semântica natural
Execução de componentes é atômica: “interleaving”
não pode ser expresso

Semântica operacional estrutural
“Interleaving” pode ser expresso facilmente
DI
UFPE
Blocos

S ::= ... | begin DV S end
DV ::= var x := a; DV | 

Semântica natural
Um sistema de transição para cada categoria sintática
DI
UFPE
Blocos
 DV,s[x  A[[a]] s ] D s’
 var x := a; DV ,s D s’
  ,s D s
 DV,s D s’
,
 S,s’ D s”
 begin DV S end,s  s” [DV(Dv)  s]
DI
UFPE
Procedimentos

S ::= ... | begin DV DP S end | call p
DV ::= var x := a; DV | 
DP ::= proc p is S; DP | 

DI
UFPE
Escopo estático para variáveis e procedimentos
Procedimentos

call p : executa o corpo de p
É
necessário registrar a associação entre nomes e
corpos de procedimentos
 Ambiente
de procedimento
EnvP = Pname  Stm  EnvV  EnvP
 Ambiente
de variável
Envv = Var  Loc
Store = Loc  { next }  Z
DI
UFPE
Procedimentos

Extensão do sistema de transições para comandos
envV, envP |- S,sto  sto’

Extensão do sistema de transições para declarações
DV,envV,sto D (env’V, sto’)
DI
UFPE
Procedimentos

Declarações
DV, envV[x  l],sto [l  v][next  new l] D (env’V ,sto’)
 var x := a; DV , envV ,sto D (env’V ,sto’)
onde v = A[[a]](sto  envV) e l = sto next
  ,envV, sto D (envV, sto)
DI
UFPE
Procedimentos

Comandos
envV, envP |- x := a,sto  sto[l  v]
onde l = envV x and v = A[[a]](sto  envV)
DV,envV, sto D (env’V ,sto’),
env’V, env’P |- S,sto’  sto”
envV, envP |-  begin DV DP S end,sto  sto”
onde env’P = updP(DP,env’V,envP)
DI
UFPE
Procedimentos
env’V, env’P |-  S,sto  sto’
envV, envP |-  call p,sto  sto’
onde envP p = (S,env’V,env’P)
env’V, env’P [p |-> (S, env’V, env’P )] |-  S,sto  sto’
envV, envP |-  call p,sto  sto’
onde envP p = (S,env’V,env’P)
DI
UFPE