The algebraic specification of abstract data types

Summary There have been many recent proposals for embedding abstract data types in programming languages. In order to reason about programs using abstract data types, it is desirable to specify their properties at an abstract level, independent of any particular implementation. This paper presents an algebraic technique for such specifications, develops some of the formal properties of the technique, and shows that these provide useful guidelines for the construction of adequate specifications.Supported in part by the National Science Foundation under grant MCS-76-06089 and the Joint Services Electronics Program monitored by the Air Force Office of the Scientific Research under contract F44620-72C-0061Supported in part by the National Research Council of Canada.     

Data types,abstract data types and their specification problem

A formal framework is proposed for discussing the algebraic properties of data types. In particular, the specification problem, i.e. the problem how a particular data type can be finitely specified, is discussed. Denotational and operational approaches are compared.     

Methodical specification of abstract data types via rewriting systems

A data type is often given by an informal model. Its formal specification is an important task, but also difficult and error-prone. Here a methodology for this task is presented. Its steps are, first, the election of a canonical form defining a canonical term algebra; second, a system of sound rewriting rules powerful enough to achieve the syntactical transformations of the canonical term algebra. The final translation of rewriting rules into equations is immediate. The methodology is illustrated by the detailed presentation of a simple example.Research partly sponsored by FINEP, CNPq and the French Ministry for Foreign Affairs.     

A practical example of the specification of abstract data types

The algebra of quotient relations, a relationally complete set of operations for data base applications, is formally defined in terms of the algebraic specification technique. The process of constructing an algebraic specification for a data type is described in order that future formal definitions are more easily derived. Several improvements to current algebraic presentation techniques are also introduced.     

Two implementation models of abstract data types

This paper compares two implementation models for abstract data types: direct and indirect implementations. Direct implementations offer relatively cheap execution and expensive compilation costs while indirect implementations result in relatively expensive implementations and cheap compilation costs. These two models are both accommodated by Ada, and a small experiment compares their costs for a particular data type.     

Algebraic implementation of abstract data types

Starting with a review of the theory of algebraic specifications in the sense of the ADJ-group a new theory for algebraic implementations of abstract data types is presented.While main concepts of this new theory were given already at several conferences this paper provides the full theory of algebraic implementations developed in Berlin except of complexity considerations which are given in a separate paper. The new concept of algebraic implementations includes implementations for algorithms in specific programming languages and on the other hand it meets also the requirements for stepwise refinement of structured programs and software systems as introduced by Dijkstra and Wirth. On the syntactical level an algebraic implementation corresponds to a system of recursive programs while the semantical level is defined by algebaic constructions, called synthesis, restriction and identification. Moreover the concept allows composition of implementations and a rigorous study of correctness. The main results of the paper are different kinds of correctness criteria which are applied to a number of illustrating examples including the implementation of sets by hash-tables. Algebraic implementations of larger systems like a histogram or a parts system are given in separate case studies which, however, are not included in this paper.     

Approximation properties of abstract data types

The well-known term model constructions for equational abstract data type specifications provide a basis for elementary semantic reasoning, but their models lack the structure necessary for reasoning about relationships between the elements. Based upon the identities supplied in the data type's specification, we define a congruence relation which describes the relative ‘answer producing’ behaviour of words in the data type language, leading to a partially ordered qoutient algebra model. For those data types whose identity sets satisfy a condition implying the Church-Rosser (confluence) property, Wadsworth's approximation property holds: the meaning of a word in the model is the least upper bound of the meanings of its ‘syntactic approximants’. Thus the model provides fixed point properties while remaining fully abstract.     

An experience in implementing abstract data types

The abstract data type concept appears to be a useful software structuring tool. A project, called ‘Système d'Objets Conservés’, which was developed at the University of Rennes, (France), gave some experience in implementing this concept. The possibility of including abstract data type into a pre-existing compiler is demonstrated, and desirable properties of the host language are exhibited. Provision of external procedures and data makes some type checking extensions necessary: these features increase software reliability.     

Enhanced abstract data types in object-relational databases

The explosion in complex multimedia content makes it crucial for database systems to support such data efficiently. This paper argues that the “blackbox” ADTs used in current object-relational systems inhibit their performance, thereby limiting their use in emerging applications. Instead, the next generation of object-relational database systems should be based on enhanced abstract data type (E-ADT) technology. An (E-ADT) can expose the semantics of its methods to the database system, thereby permitting advanced query optimizations. Fundamental architectural changes are required to build a database system with E-ADTs; the added functionality should not compromise the modularity of data types and the extensibility of the type system. The implementation issues have been explored through the development of E-ADTs in Predator. Initial performance results demonstrate an order of magnitude in performance improvements. Received January 1, 1998 / Accepted May 27, 1998     

Verifying abstract data types with SNOBOL4

The presentation of an abstract data type by a series of equational axioms has become an accepted specification mechanism. Verifying the correctness of such specifications has been recognized as a problem troubling their use. A means is presented for experimenting with a directly executable version of the axioms without having to choose representations for the data structures or describe algorithms for the operations.     

Computability and implementability issues in abstract data types

In a strongly typed system supporting user-defined data abstractions, the designer of a data abstraction ought to be careful in choosing the operations for the abstraction. If the operation set chosen is not expressive enough, it might be impossible or inconvenient to implement certain useful functions on the values of the data abstraction. In this paper, two properties of the operation set of a data abstraction, expressive completeness and expressive richness, are defined to formally characterize the expressive power of the operation set.For an expressively complete data abstraction, the operation set is powerful enough to implement in principle all computable properties of the values, whereas for an expressively rich data abstraction, the operation set can be used to implement the properties in a ‘simple and natural’ fashion. It is shown that if the equality predicate on the values of a data abstraction can be implemented in terms of its operations, then the data abstraction is expressively complete.For expressive richness, we identify a finite set of functions that represent certain basic kinds of manipulations of the values, and require them to be implemented in terms of the operation set as ‘straight line’ programs. The relation between these formal properties and the intuitive notions are considered. We argue that it is important to consider both expressive completeness and expressive richness while designing the operation set of a data abstraction. Practical applications of the properties of expressiveness introduced are also discussed.     

Synthesizing implementations of abstract data types from axiomatic specifications

This paper describes a system for automatically generating an implementation of an abstract data type from its axiomatic specifications. Such a system can be useful for rapid prototyping and for detecting inconsistencies in the specifications by testing the generated implementation. In the generated Implementation, an instance of the data type is represented by its state. An operation on the data type is implemented by a collection of functions — a function for each of the axioms specified for the operation, and a function for the operation that determines, depending on the state of the instance(s) on which the operation is being performed, which of the axioms of the operation is applicable. The system is developed on a Sun-3 workstation running Unix. It is written in C and generates the implementation of the abstract data type in C.     

Algebraic specification of data types: A synthetic approach

A mathematical interpretation is given to the notion of a data type, which allows procedural data types and circularly defined data types. This interpretation seems to provide a good model for what most computer scientists would call data types, data structures, types, modes, clusters or classes. The spirit of this paper is that of McCarthy [43] and Hoare [18]. The mathematical treatment is the conjunction of the ideas of Scott on the solution of domain equations [34], [35], and [36] and the initiality property noticed by the ADJ group (ADJ [2] and [3]). The present work adds operations to the data types proposed by Scott and proposes an alternative to the equational specifications proposed by Guttag [14], Guttag and Horning [15] and ADJ [2]. The advantages of such a mathematical interpretation are the following: throwing light on some ill-understood constructs in high-level programming languages, easing the task of writing correct programs and making possible proofs of correctness for programs or implementations.This research was conducted at the University of Warwick while both authors were supported by the Science Research Council grant B/RG 31948 to D. Park and M. Paterson. During the final redaction of the paper the first author was partially supported by the National Science Foundation grant MCS78-07461. EDITOR'S NOTE: This paper is one of several invited for submission to this journal to present different approaches to the subject of the semantics of programming languages.     

Characterization theorems on abstract families of transducers

For an AFL /oL and an AFT /oM, /oM(/oL) denotes the family of languages obtained from languages in /oL by imposing transformations through transducers in /oM. Then /oM (/oL) is a full AFL. Two characterization theorems of /oM (/oL) are given. One is in terms of homomorphism and intersection, and the other is in terms of AFA with control set.     

Computer-aided proofs of Arrow's and other impossibility theorems

Arrow's impossibility theorem is one of the landmark results in social choice theory. Over the years since the theorem was proved in 1950, quite a few alternative proofs have been put forward. In this paper, we propose yet another alternative proof of the theorem. The basic idea is to use induction to reduce the theorem to the base case with 3 alternatives and 2 agents and then use computers to verify the base case. This turns out to be an effective approach for proving other impossibility theorems such as Muller-Satterthwaite and Sen's theorems as well. Motivated by the insights of the proof, we discover a new theorem with the help of computer programs. We believe this new proof opens an exciting prospect of using computers to discover similar impossibility or even possibility results.     

Replicated abstract data types: Building blocks for collaborative applications

For distributed applications requiring collaboration, responsive and transparent interactivity is highly desired. Though such interactivity can be achieved with optimistic replication, maintaining replica consistency is difficult. To support efficient implementations of collaborative applications, this paper extends a few representative abstract data types (ADTs), such as arrays, hash tables, and growable arrays (or linked lists), into replicated abstract data types (RADTs). In RADTs, a shared ADT is replicated and modified with optimistic operations. Operation commutativity and precedence transitivity are two principles enabling RADTs to maintain consistency despite different execution orders. Especially, replicated growable arrays (RGAs) support insertion/deletion/update operations. Over previous approaches to the optimistic insertion and deletion, RGAs show significant improvement in performance, scalability, and reliability.     

Programming abstract data types,iterators and generic modules in C

A programming discipline to write abstract data types, iterators and generic modules using the C language is proposed. Program examples are presented making use of features of the ANSI standard for C. The discipline supports object-oriented development by allowing the programmer to implement abstractions through modules with well-defined interfaces. To use the abstractions, the programmer is not required to be aware of how they are implemented.