Semântica operacional estruturada

Origem: Wikipédia, a enciclopédia livre.

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 contruçõ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.

[editar] 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 substituida pelo valor $A [a] s$ (veja a definição da função semântica $A$ no artigo semântica formal).