10 - The mathematical basis of abstract data types

Summary

In Chapter 7 we discussed the desired logical relationships between segments of program and their specifications. In that discussion it was sufficient to take for granted all the common properties of integers, etc., and to concentrate on the more important (deductive) issues. However, in order to make our arguments mathematically sound we must explain how these ‘facts’ are introduced into a programming system. The method, outlined below, not only gives a foundation for the mathematical manipulations that are central to our methodology, but also provides a set of requirements against which implementations can be checked, and can also be applied to (abstract) data types which may not be native to the target computer system.

We begin, in Section 10.1, with a look at probably the most fundamental data type, Boolean. Objects and expressions of type Boolean are required in one form or another in all programming languages to control the flow of a computation. They are also used to manipulate tests associated with other, more explicitly data-related, types and since the type has only two data values we can defer consideration of problems associated with large, potentially infinite, sets of data values.

Next, in Section 10.2, we look at lists. Constructing a list-of-something is one of the more familiar ways of building a new type from an existing one. Although a set of lists may be infinite, lists provide a vehicle for the introduction of more facilities of our definition system before going on to discussing problems associated with numeric types in Section 10.3.