Towards a Theory for Abstract Data Types.

A rigorous framework for studying immutable data types having nondeterministic operations and operations exhibiting exceptional behavior is developed. The framework embodies the view of a data type taken in programming languages, and supports hierarchical and modular structure among data types. The central notion in this framework is the definition of a data type. An algebraic and behavioral approach for defining a data type is developed which focuses on the input-output behavior of a data type as observed through its operations. The definition of a data type abstracts from the representational structure of its values as well as from the multiple representations of the values for any representational structure. A hierarchical specification language for data types is proposed. A deductive system based on first order multi-sorted predicate calculus with identity is developed for abstract data types. A correctness criterion is proposed for an implementation coded in a programming language with respect to a specification. It is defined as a relation between the semantics of an implementation and the semantics of a specification. It does not require a correct implementation to have the maximum amount of nondeterminism specified by a specification. A methodology for proving correctness of an implementation is developed which embodies the correctness criterion.