Semântica formal

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

Nota: Para outros significados de Semântica, ver Semântica (desambiguação).

Semântica formal é a área de estudo de ciência da computação que preocupa-se em especificar o significado (ou comportamento) de programas de computador e partes de hardware.

A semântica é complementar a sintaxe de programas de computador, que preocupa-se em descrever as estruturas de uma linguagem de programação.

A necessidade de uma semântica formal (matemática) para linguagens de programação justifica-se pois:

Pode revelar ambigüidades na definição da linguagem (o que uma descrição não formal não permitiria revelar);
É uma base para implementação (síntese), análise e verificação formal.

Índice

1 Abordagens
2 Funções semânticas e semântica de expressões
3 Ver também
4 Referências

[editar] Abordagens

Existem três principais abordagens para desenvolver a especificação da semântica:

Semântica operacional - Nesta abordagem 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;
Semântica denotacional - Os significados são modelados por objetos matemáticos, geralmente funções semânticas definidas composicionalmente, que representam o efeito de executar uma estrutura. Isto significa que o efeito interessa mais que como é produzida a computação;
Semântica axiomática - Neste caso, se especifica propriedades do efeito da execução das estruturas como asserções , que são sentenças da lógica de predicados. Estas sentenças são usualmente chamadas de axiomas, e daí o nome desta abordagem. Alguns aspectos da execução são ignorados.

A abordagem Operacional, por sua vez, possui duas versões:

Semântica operacional estruturada - Especifica mais detalhes da execução, tomando um passo menor;
Semântica natural - Simplifica a notação e esconde detalhes, ao tomar um passo maior.

Existem também abordagens de semântica formal baseadas em redes de Petri e lógica temporal.

Finalmente, ainda existem abordagens baseadas em teoria das categorias, comumente chamadas pelo nome comum de semântica categorial. Neste caso, as funções semânticas são definidas usando-se noções categoriais de morfismos e composicionalidade. Esta abordagem tira proveito da expressividade de teoria das categorias, e está relacionada com a abordagem denotacional.

[editar] Funções semânticas e semântica de expressões

A definição da semântica de linguagens faz uso de funções semânticas que se aplicam sobre as estruturas da linguagem e lhes dão significado. Neste tipo de definição usam-se estados que definem os valores das variáveis em um determinado momento.

Um exemplo de função semântica é dado por:

$A [a 1 + a 2] s = A [a 1] s + A [a 2] s$

onde: $s=[x\mapsto 10,y\mapsto 5]$ define um estado em que a variável x vale 10 e a variável y vale 5.

A função $A$ é um exemplo simples de função semântica usada para avaliação de expressões aritméticas. A seqüência acima significa que a expressão $a 1 + a 2$ será avaliada no estado $s$ como sendo a soma da avaliação das subexpressões $a 1$ e $a 2$ neste mesmo estado.