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 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.

Grantor dc:publisher

Universidad de La Rioja (España)

Year dc:date

2002

Author dc:creator

• Pascual Martínez Losa, María Vico

Contributors dc:contributor

• Lambán Pardo, Laureano (Universidad de La Rioja)
• Rubio García, Julio (Universidad de La Rioja)

Statement dc:rights

• LICENCIA 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

Language dc:language

spa

Identifier

(Tesis) ISBN 84-688-0904-7

OAI identifier oai:identifier

oai:dialnet.unirioja.es:TES0000000006