Objetos localmente efectivos y tipos abstractos de datos

Abstract

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.