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.

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.