Hispanopedia WikiLa 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 de investigación en ciencias de la computación alrededor de 1980. [ 5 ]
Descripción general
La especificación algebraica busca desarrollar sistemáticamente programas más eficientes mediante:
- definir formalmente los tipos de datos y las operaciones matemáticas sobre esos tipos de datos.
- abstraer detalles de implementación, como el tamaño de las representaciones (en memoria) y la eficiencia de obtención del resultado de los cálculos.
- formalizar los cálculos y operaciones sobre tipos de datos
- lo que permite la automatización al restringir formalmente las operaciones a este conjunto limitado de comportamientos y tipos de datos.
Una especificación algebraica logra estos objetivos definiendo uno o más tipos de datos y especificando un conjunto de funciones que operan sobre esos tipos de datos. Estas funciones se pueden dividir en dos clases:
- Funciones constructoras : Funciones que crean o inicializan los elementos de datos, o que construyen elementos complejos a partir de otros más simples. El conjunto de funciones constructoras disponibles viene implícito en la firma de la especificación . Además, una especificación puede contener ecuaciones que definen equivalencias entre los objetos construidos por estas funciones. Que la representación subyacente sea idéntica para construcciones diferentes pero equivalentes depende de la implementación.
- Funciones adicionales : Funciones que operan sobre los tipos de datos y que se definen en términos de las funciones constructoras.
Ejemplos
Consideremos una especificación algebraica formal para el tipo de dato booleano .
Una posible especificación algebraica podría proporcionar dos funciones constructoras para el elemento de datos: una constructora para verdadero y otra para falso . De esta forma, se podría declarar, construir e inicializar un elemento de datos booleano con un valor. En este caso, todos los demás elementos conectivos , como XOR y AND , serían funciones adicionales . Así, se podría instanciar un elemento de datos con un valor "verdadero" o "falso", y se podrían usar funciones adicionales para realizar cualquier operación sobre dicho elemento.
Alternativamente, todo el sistema de tipos de datos booleanos podría especificarse utilizando un conjunto diferente de funciones constructoras: un constructor falso y un constructor no . En ese caso, se podría definir una función adicional verdadera para producir el valor no falso y una ecuación.debería añadirse.
Por lo tanto, la especificación algebraica describe todos los estados posibles del elemento de datos y todas las transiciones posibles entre estados.
Para un ejemplo más complejo, 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 sugerir 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 terminante, que asigna a cualquier término construido una forma normal inequívoca que representa el entero correspondiente:
... (((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 cumpla con esta especificación se comportará como los números enteros, o posiblemente como un rango restringido de ellos, como los tipos de enteros habituales que se encuentran en la mayoría de los lenguajes de programación.
Véase también
Notas
- ↑ Ehrig, Hartmut ; Mahr, Bernd (1989). Especificación algebraica . Academic Press. ISBN 0-201-41635-2.
- ↑ Bergstra, JA; Heering, J.; Klint, J. (1985). Especificación algebraica . Monografías de EATCS sobre informática teórica. Vol. 6. Springer-Verlag.
- ↑ Wirsing, Martin (1990). Jan van Leeuwen (ed.). Especificación algebraica . Manual de informática teórica. Vol. B. Elsevier. págs. 675–788 .
- ↑ Sannella, Donald; Tarlecki, Andrzej (2012). Fundamentos de la especificación algebraica y el desarrollo formal de software . Monografías de EATCS sobre informática teórica. Springer-Verlag. ISBN 978-3-642-17335-6.
- ↑ Wagner, Eric G. (diciembre de 2002). «Especificaciones algebraicas: algo de historia y nuevas ideas» . Nordic Journal of Computing . 9 (4): 373–404 . ISSN 1236-6064 . Archivado del original el 30 de agosto de 2003.
- Métodos formales
