Partial Implementations of Abstract Data Types: Theory and Practice

201 p.Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1988.We propose the use of partial implementations of abstract data types as a solution to the partiality problem which arises in the top-down development of programs. In the main, this problem consists in the inability to implement all of an ideal abstract type by a program, though it has other aspects. We explain why we believe the partial implementation approach to be superior to other solutions to the partiality problem, and show how it can be used in a sound manner in the development process.To study the practicality of the approach, we begin by considering what is required of a partial implementation, and develop two criteria which guarantee partial implementation: the H-criterion (for homomorphism), which comes closest to the usual criterion for total implementation, and the GH-criterion (for generalized homomorphism). We then investigate whether the methods for proving total implementation associated with several known specification methods can be adapted to methods for proving partial implementation by our criteria. We show that while those for equational specifications are not particularly suited to this purpose, those for other types of specifications, in particular, final algebra and pre-post specifications, are adaptable. We find the GH-criterion--which involves existence of a relation rather than a map with certain properties, and is nearly the most general possible criterion for partial implementation--to be more useful in many circumstances.We then consider the problems that the partial implementation approach entails for parameterized types. In incremental program development, it is possible for the parameter to a parameterized type to be implemented before the parameterized type itself. The use of partial implementations thus implies the need to extend the usual semantics of specifications of parameterized types to allow for parameter algebras of arbitrary partiality. We attempt to de this for final algebra specifications and equational specifications. Our results show final algebra specifications to be more desireable for our purposes, since the natural extension to their semantics preserves implementations by the GH-criterion. For initial algebra specifications, the extension we obtain preserves implementations by the H-criterion, but not the GH-criterion, except for total algebra parameters.U of I OnlyRestricted to the U of I community idenfinitely during batch ingest of legacy ETD