Especificação algébrica

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Question book.svg
Esta página ou se(c)ção não cita fontes fiáveis e independentes (desde Março de 2008). Por favor, adicione referências e insira-as no texto ou no rodapé, conforme o livro de estilo. Conteúdo sem fontes poderá ser removido.
Searchtool.svg
Esta página ou secção foi marcada para revisão, devido a inconsistências e/ou dados de confiabilidade duvidosa. Se tem algum conhecimento sobre o tema, por favor verifique e melhore a consistência e o rigor deste artigo. Pode encontrar ajuda no WikiProjeto Ciência da computação.

Se existir um WikiProjeto mais adequado, por favor corrija esta predefinição. Este artigo está para revisão desde Julho de 2009.

Em ciência da computação, especificação algébrica (ou especificação formal) é área de estudos que define métodos matemáticos rigorosos com vista ao desenvolvimento de programas correctos e eficientes.

Uma especificação consiste na declaração de operações] e tipos (ou géneros) e posteriormente na declaração por meio de equações das propriedades que essas operações devem obedecer. Após a fase de especificação pode-se proceder a testes por meio de exemplos cujo sistema deverá verificar formalmente. No entanto, alguns exemplos podem ser dedutíveis mas outros não.

Uma álgebra e operações relacionadas (por exemplo, os naturais e operações como soma) é então associada a uma especificação tornando-se numa implementação da especificação algébrica.

O refinamento é um processo da especificação algébrica que consiste na procura de uma álgebra o mais pequena possível para um dado problema. Sucessivos refinamentos permitem reduzir a álgebra.