Semântica operacional estruturada

Semântica operacional estruturada é uma das abordagens de semântica formal. A semântica formal é uma das áreas de estudo de ciência da computação, preocupada em atribuir significado às construções das linguagens de programação.

Na semântica operacional, o significado de uma construção da linguagem é especificado pela computação que ela induz quando executada em uma máquina hipotética. Isto significa que interessa mais como o efeito da computação é produzido.

A semântica operacional estruturada é uma versão de semântica operacional em que se especifica mais detalhes da execução, tomando um passo menor. Isto significa que os cálculos são mais longos, porém eles detalham melhor os passos da computação de um programa.

A semântica operacional estruturada foi proposta por G. Plotkin em 1981, no artigo clássico "A Structural Approach to Operational Semantics", como um refinamento à semântica operacional.

Transições e regras

A definição da semântica operacional estruturada faz uso de uma relação de transição $<S,s>\Rightarrow s'$, que significa que o comando $S$ iniciando no estado $s$ finaliza sua execução no estado $s'$, e de um conjunto de regras que define as transições possíveis. Por exemplo,

$<x:=a,s>\Rightarrow s[x\mapsto A[a]s]$

significa que a atribuição $x:=a$ será avaliada no estado $s$ como sendo a transição que conduz ao estado em que a variável $x$ foi substituída pelo valor $A[a]s$ (veja a definição da função semântica $A$ no artigo semântica formal).

Ver também

• Semântica formal
• Ciência da computação
• Linguagens de programação
• Linguagens formais e compiladores

Referências

• Nielson, H. & Nielson, F. Semantics with Applications: a formal introduction. disponível em: http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html
• Lâminas para curso de um semestre de duração de semântica formal a nível de graduação

Leitura adicional

• G. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Aarhus University, 1981.