Abstract: A theory of data abstraction in modular programming is presented that explains why this technique leads to correct programs.
Data abstraction allows users and implementers to take different views of a specification: While users may depend on a specification as it is, implementers need not provide program entities that satisfy the specification, but merely a ``representation'' of such entities. This means that the users may be supplied with program entities that do not satisfy the specification, and so it is necessary to explain why their code functions correctly nevertheless.
It is shown that data abstraction leads to correct programs if the modules of the programs are ``stable'', and it is suggested that programming languages for data abstraction should guarantee stability for their modules. The stability criterion corresponds closely to the intuitive idea of ``limited access'' to encapsulated data types, and to ``representation independence'' properties of the typed lambda-calculus.
The theory is developed in the general framework of an ``institution'' and uses an abstract notion of ``representation''. Specifically, the institution of partial many-sorted algebras is considered and the representation relations ``behavioural inclusion'', ``behavioural equivalence'' and ``standard representation'' (the popular concept based on abstraction functions) are studied. These representation relations are characterized by certain many-sorted relations between algebras, called ``correspondences'', which provide useful practical proof methods for the correctness of data representations.
Behavioural equivalence is found to be superior to standard representation in that ``representation bias'' of a specification no longer restricts its range of implementations, and in that it allows more constructs to be included in a data abstraction programming language.
Ph.D. thesis - Price £8.50
LFCS report ECS-LFCS-87-19Previous | Index | Next