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.