Especificação algébrica - Algebraic specification

A especificação algébrica é uma técnica de engenharia de software para especificar formalmente o comportamento do sistema. Foi um assunto muito ativo de pesquisa em ciência da computação por volta de 1980.

Visão geral

A especificação algébrica busca desenvolver sistematicamente programas mais eficientes:

  1. definir formalmente tipos de dados e operações matemáticas nesses tipos de dados
  2. abstrair detalhes de implementação, como o tamanho das representações (na memória) e a eficiência de obtenção do resultado dos cálculos
  3. formalizar os cálculos e operações em tipos de dados
  4. permitindo a automação restringindo formalmente as operações a este conjunto limitado de comportamentos e tipos de dados.

Uma especificação algébrica atinge esses objetivos definindo um ou mais tipos de dados e especificando uma coleção de funções que operam nesses tipos de dados. Essas funções podem ser divididas em duas classes:

  1. funções construtoras : funções que criam ou inicializam os elementos de dados ou constroem elementos complexos a partir dos mais simples
  2. funções adicionais : funções que operam nos tipos de dados e são definidas em termos das funções do construtor.

Exemplo

Considere uma especificação algébrica formal para o tipo de dados booleano .

Uma possível especificação algébrica pode fornecer duas funções construtoras para o elemento de dados: um construtor verdadeiro e um construtor falso . Assim, um elemento de dados booleano pode ser declarado, construído e inicializado com um valor. Nesse cenário, todos os outros elementos conectivos , como XOR e AND , seriam funções adicionais . Assim, um elemento de dados pode ser instanciado com valor "verdadeiro" ou "falso", e funções adicionais podem ser usadas para executar qualquer operação no elemento de dados.

Alternativamente, todo o sistema de tipos de dados booleanos pode ser especificado usando um conjunto diferente de funções de construtor: um construtor falso e um não construtor. Nesse caso, uma função adicional poderia ser definida para gerar o valor "verdadeiro".

A especificação algébrica, portanto, descreve todos os estados possíveis do elemento de dados e todas as transições possíveis entre os estados.

Veja também

Notas


Ícone de esboço

Este artigo é um esboço sobre ciência . Você pode ajudar a Wikipedia expandindo-a .