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 editar

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

 

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

Ver também editar

Referências editar

Leitura adicional editar

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