Objetos localmente efectivos y tipos abstractos de datos

There are a lot of techniques that allow to tackle the problem of verifying whether a program runs correctly, that is, in the way intended by the user. This doctoral thesis represents a contribution to the analysis of the data types handled by programs. Particularly, we focused on the modelling of d...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Pascual Martínez Losa, María Vico
Otros Autores:	Lambán Pardo, Laureano (Universidad de La Rioja)
Formato:	text (thesis)
Lenguaje:	spa
Publicado:	Universidad de La Rioja (España) 2002
Acceso en línea:	https://dialnet.unirioja.es/servlet/oaites?codigo=63
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

id	oai-TES0000000006
record_format	dspace
institution	DialNet
collection	DialNet
language	spa
description	There are a lot of techniques that allow to tackle the problem of verifying whether a program runs correctly, that is, in the way intended by the user. This doctoral thesis represents a contribution to the analysis of the data types handled by programs. Particularly, we focused on the modelling of data structures in a Symbolic Computation system called EAT (Effective Algebraic Topology) designed by Rubio and Sergeraert. EAT is a Common Lisp system devoted to Algebraic Topology and a tool for the mechanized computation of homology groups of infinite topological spaces (namely, iterated loop spaces). In order to perform a formal analysis of the EAT data structures, an operation on Abstract Data Types is defined. This operation (defined within the classical Algebraic Specification framework) is inspired by the EAT way of working with complex mathematical structures. Looking for a connection with the current mainstream topics in the field of Algebraic Specification, we found that our approach was closely related to some object-oriented formalisms, namely, hidden specifications and the coalgebraic view. These relations made explicit the implicit object-oriented features of the EAT system. This was unexpected since the crux in EAT is the role of the functional programming. The main tool used is a syntactic operation between signatures, denoted ()imp, which is extended to Abstract Data Types and intends to capture the EAT way of working. This operation constructs from an abstract data type T a new abstract data type, Timp, which should be considered as the abstract data type of the implementations of T. We established an implementation framework in which we proved that the EAT data structures used are implementations of Timp abstract data types. Moreover, we obtained mathematical results that characterize the EAT data structures as coproducts and final objects in certain categories of implementations. These results allow us to claim that the EAT way of implementation has appropriate properties. The characterization of the EAT data structures obtained includes those coding algebraic structures of finite nature, called Effective Objects, as well as those coding information of infinite nature, called Locally Effective Objects.
author2	Lambán Pardo, Laureano (Universidad de La Rioja)
author_facet	Lambán Pardo, Laureano (Universidad de La Rioja) Pascual Martínez Losa, María Vico
format	text (thesis)
author	Pascual Martínez Losa, María Vico
spellingShingle	Pascual Martínez Losa, María Vico Objetos localmente efectivos y tipos abstractos de datos
author_sort	Pascual Martínez Losa, María Vico
title	Objetos localmente efectivos y tipos abstractos de datos
title_short	Objetos localmente efectivos y tipos abstractos de datos
title_full	Objetos localmente efectivos y tipos abstractos de datos
title_fullStr	Objetos localmente efectivos y tipos abstractos de datos
title_full_unstemmed	Objetos localmente efectivos y tipos abstractos de datos
title_sort	objetos localmente efectivos y tipos abstractos de datos
publisher	Universidad de La Rioja (España)
publishDate	2002
url	https://dialnet.unirioja.es/servlet/oaites?codigo=63
work_keys_str_mv	AT pascualmartinezlosamariavico objetoslocalmenteefectivosytiposabstractosdedatos
_version_	1718346545394352128
spelling	oai-TES00000000062016-04-13Objetos localmente efectivos y tipos abstractos de datosPascual Martínez Losa, María VicoThere are a lot of techniques that allow to tackle the problem of verifying whether a program runs correctly, that is, in the way intended by the user. This doctoral thesis represents a contribution to the analysis of the data types handled by programs. Particularly, we focused on the modelling of data structures in a Symbolic Computation system called EAT (Effective Algebraic Topology) designed by Rubio and Sergeraert. EAT is a Common Lisp system devoted to Algebraic Topology and a tool for the mechanized computation of homology groups of infinite topological spaces (namely, iterated loop spaces). In order to perform a formal analysis of the EAT data structures, an operation on Abstract Data Types is defined. This operation (defined within the classical Algebraic Specification framework) is inspired by the EAT way of working with complex mathematical structures. Looking for a connection with the current mainstream topics in the field of Algebraic Specification, we found that our approach was closely related to some object-oriented formalisms, namely, hidden specifications and the coalgebraic view. These relations made explicit the implicit object-oriented features of the EAT system. This was unexpected since the crux in EAT is the role of the functional programming. The main tool used is a syntactic operation between signatures, denoted ()imp, which is extended to Abstract Data Types and intends to capture the EAT way of working. This operation constructs from an abstract data type T a new abstract data type, Timp, which should be considered as the abstract data type of the implementations of T. We established an implementation framework in which we proved that the EAT data structures used are implementations of Timp abstract data types. Moreover, we obtained mathematical results that characterize the EAT data structures as coproducts and final objects in certain categories of implementations. These results allow us to claim that the EAT way of implementation has appropriate properties. The characterization of the EAT data structures obtained includes those coding algebraic structures of finite nature, called Effective Objects, as well as those coding information of infinite nature, called Locally Effective Objects.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.Universidad de La Rioja (España)Lambán Pardo, Laureano (Universidad de La Rioja)Rubio García, Julio (Universidad de La Rioja)2002text (thesis)application/pdfhttps://dialnet.unirioja.es/servlet/oaites?codigo=63(Tesis) ISBN 84-688-0904-7 spaLICENCIA DE USO: Los documentos a texto completo incluidos en Dialnet son de acceso libre y propiedad de sus autores y/o editores. Por tanto, cualquier acto de reproducción, distribución, comunicación pública y/o transformación total o parcial requiere el consentimiento expreso y escrito de aquéllos. Cualquier enlace al texto completo de estos documentos deberá hacerse a través de la URL oficial de éstos en Dialnet. Más información: https://dialnet.unirioja.es/info/derechosOAI \| INTELLECTUAL PROPERTY RIGHTS STATEMENT: Full text documents hosted by Dialnet are protected by copyright and/or related rights. This digital object is accessible without charge, but its use is subject to the licensing conditions set by its authors or editors. Unless expressly stated otherwise in the licensing conditions, you are free to linking, browsing, printing and making a copy for your own personal purposes. All other acts of reproduction and communication to the public are subject to the licensing conditions expressed by editors and authors and require consent from them. Any link to this document should be made using its official URL in Dialnet. More info: https://dialnet.unirioja.es/info/derechosOAI

Objetos localmente efectivos y tipos abstractos de datos

Ejemplares similares