La especificación algebraica [1] [2] [3] [4] es una técnica de ingeniería de software para especificar formalmente el comportamiento del sistema. Fue un tema muy activo en la investigación informática alrededor de 1980. [5]
La especificación algebraica busca desarrollar sistemáticamente programas más eficientes mediante:
Una especificación algebraica logra estos objetivos definiendo uno o más tipos de datos y especificando una colección de funciones que operan sobre esos tipos de datos. Estas funciones se pueden dividir en dos clases:
Considere una especificación algebraica formal para el tipo de datos booleano .
Una posible especificación algebraica puede proporcionar dos funciones constructoras para el elemento de datos: un constructor verdadero y un constructor falso . Por lo tanto, un elemento de datos booleano podría declararse, construirse e inicializarse con un valor. En este escenario, todos los demás elementos conectivos , como XOR y AND , serían funciones adicionales . Por lo tanto, un elemento de datos podría instanciarse con un valor "verdadero" o "falso", y podrían usarse funciones adicionales para realizar cualquier operación en el elemento de datos.
Como alternativa, se podría especificar todo el sistema de tipos de datos booleanos utilizando un conjunto diferente de funciones constructoras: un constructor false y un constructor not . En ese caso, se podría definir una función adicional true para obtener el valor not false y se debería agregar una ecuación.
Por lo tanto, la especificación algebraica describe todos los estados posibles del elemento de datos y todas las transiciones posibles entre estados. [ cita requerida ]
Para un ejemplo más complicado, los números enteros se pueden especificar (entre muchas otras formas, y eligiendo uno de los muchos formalismos) con dos constructores.
1 : Z (_ - _) : Z×Z -> Z
y tres ecuaciones:
(1 - (1 - p)) = p ((1 - (n - p)) - 1) = (p - n) ((p1 - n1) - (n2 - p2)) = (p1 - (n1 - (p2 - n2)))
Es fácil verificar que las ecuaciones son válidas, dada la interpretación habitual de la función binaria "menos". (Los nombres de las variables se han elegido para indicar contribuciones positivas y negativas al valor). Con un poco de esfuerzo, se puede demostrar que, aplicadas de izquierda a derecha, también constituyen un sistema de reescritura confluente y terminal, que asigna cualquier término construido a una forma normal inequívoca que representa el número entero respectivo:
... (((1 - 1) - 1) - 1) ((1 - 1) - 1) (1 - 1) 1 (1 - ((1 - 1) - 1)) (1 - (((1 - 1) - 1) - 1)) ...
Por lo tanto, cualquier implementación que se ajuste a esta especificación se comportará como los números enteros, o posiblemente un rango restringido de ellos, como los tipos de números enteros habituales que se encuentran en la mayoría de los lenguajes de programación.
