Objetos localmente efectivos y tipos abstractos de datos

Resumen

Existen muchas técnicas que permiten abordar, parcialmente, uno de los problemas centrales en Informática Aplicada: el problema de verificar si un programa funciona correctamente, es decir, si funciona como los usuarios esperan de él. En esta tesis se realizan aportaciones en el análisis de los tipos de datos manipulados por los programas. Concretamente, el trabajo se centra en modelar las estructuras de datos que aparecen en un sistema de Cálculo Simbólico denominado EAT (Effective Algebraic Topology) diseñado por Rubio y Sergeraert. EAT es un sistema escrito en Common Lisp y dedicado a realizar cálculos en Topología Algebraica. Ha resultado ser útil para calcular grupos de homología de espacios topológicos infinitos (en concreto, espacios de lazos iterados). Para realizar el análisis formal de las estructuras de datos del sistema EAT, se define una operación entre Tipos Abstractos de Datos (en el marco clásico de Especificación Algebraica?, inspirada por la forma en la que EAT trabajo con estructuras matemáticas complejas. Al buscar relaciones con los tópicos actuales en el campo de Especificación Algebraica, encontramos que nuestra aproximación está muy relacionada con algunos formalismos orientados a objeto, concretamente con las especificaciones ocultas y el marco coalgebraico. Estas relaciones hacen explícitas las características orientadas a objeto implícitas del sistema EAT. La principal herramienta utilizada es una operación sintáctica entre signaturas, denotada ()imp, que se extiende a Tipos Abstractos de Datos y que pretende recoger la forma de trabajar de EAT. Esta operación construye, a partir de un tipo abstracto de datos T, un nuevo tipo abstracto de datos, Timp, que debería considerarse como el tipo abstracto de datos de las implementaciones de T. Además, establecemos un marco de implementación en el que probamos que las estructuras de datos utilizadas en EAT son implementaciones de tipos abstractos de datos Timp. En este marco se obtienen resultados matemáticos que caracterizan a las estructuras de datos de EAT como coproductos y objetos finales en ciertas categorías de implementaciones, lo que nos permite afirmar que la forma de implementación de EAT posee las propiedades adecuadas. Esta caracterización recoge tanto a las estructuras de datos que codifican estructuras algebraicas de naturaleza finita, denominadas Objetos Efectivos, como a las que codifican información de naturaleza infinita, denominadas Objetos Localmente Efectivos.