Especificação algébrica

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.^[1][2][3]

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.

Referências

1. Ehrig, H.; B. Mahr (1989). Algebraic Specification. [S.l.]: Academic Press. ISBN 0-201-41635-2
2. Bergstra, J.A.; J. Heering; J. Klint (1985). Algebraic Specification. Col: EATCS Monographs on Theoretical Computer Science. 6. [S.l.]: Springer-Verlag
3. Wirsing, M. (1990). Jan van Leeuwen, ed. Algebraic Specification. Col: Handbook of Theoretical Computer Science. B. [S.l.]: Elsevier. pp. 675–788