Semântica formal

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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 ambigüidades 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[editar | editar código-fonte]

Existem quatro principais abordagens para desenvolver a especificação da semântica:

  • Semântica de Contextos e Cenários - SCC - Abordagem semântica desenvolvida por Celso Ferrarezi Junior, a Semântica de Contextos e Cenários é uma vertente dos estudos em Semântica Cultural. Essa abordagem se baseia na ideia que, entre outras funções, uma língua natural atua como uma forma de representação culturalmente determinada e que, portanto, só tem funcionamento pleno e adequado no ambiente cultural para o qual cada representação foi concebida. Isso implica reconhecer que, até mesmo na estrutura gramatical de uma língua natural, se manifestam traços da cultura dos falantes como, por exemplo, na construção de classes de palavras e no processo de atribuição de sentidos às unidades da língua. Essa vertente de estudos assume que a forma como representamos o mundo em nossa comunidade é também a forma como o recebemos, de maneira que se constrói uma inter-relação entre linguagem, pensamento e cultura. A SCC assume que o objeto de estudo da semântica é o sentido e não o significado, como tradicionalmente concebido.
  • 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:

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[editar | editar código-fonte]

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.

Bibliografia[editar | editar código-fonte]

Ver também[editar | editar código-fonte]