Semântica formal
Nota: Para outros significados de Semântica, veja Semântica (desambiguação).Semântica formal é a área de estudo de ciência da computação que se preocupa em especificar o significado (ou comportamento) de programas de computador e partes de hardware.
A semântica é complementar à sintaxe de programas de computador, que se preocupa 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 ambiguidades na definição da linguagem (o que uma descrição informal não permitiria revelar);
- É uma base para implementação (síntese), análise e verificação formal.
Abordagens
editarExistem 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.
Funções semânticas e semântica de expressões
editarA 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:
![{\displaystyle A[a_{1}+a_{2}]s=A[a_{1}]s+A[a_{2}]s}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9a0573122a6eda26423f1478b9a3ab1983ad1b8f)
onde: define um estado em que a variável x vale 10 e a variável y vale 5.
![{\displaystyle s=[x\mapsto 10,y\mapsto 5]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/92ec6f2edb303d189f4a730b873cc3c56b38be78)
A função é um exemplo simples de função semântica usada para avaliação de expressões aritméticas. A sequência acima significa que a expressão será avaliada no estado como sendo a soma da avaliação das subexpressões e neste mesmo estado.
Bibliografia
editar- 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 em nível de graduação