A theory of objects. (English) Zbl 0876.68014

New York, NY: Springer-Verlag. xiii, 396 p. (1996).
This book develops a theory of objects as a foundation for object-oriented languages and programming. The authors take objects as primitive and concentrate on the intrinsic rules that objects should obey. By doing so, they introduce a family of object calculi and develop a theory of objects around them. Using these object calculi, the authors explain both the semantics of objects and their typing rules. They account for a broad range of crucial object-oriented concepts, such as the Self type, dynamic dispatch, classes, inheritance, prototyping, subtyping, covariance and contravariance, and method specialization. Because of the compactness of object calculi they are likely to serve as a convenient basis for research on specification, verification, and analysis of object-oriented programs. The book begins with an informal review of object-oriented concepts, trying to characterize the fundamental features of object-oriented languages.
The main body of the book is divided into three parts, where the authors discuss semantic, typing and programming structures of growing sophistication using increasingly higher-ordered calculi. At the end of each part, an object-oriented programming language is presented that embodies the main features considered in that part. In the first part, a tiny untyped (Smalltalk-style) object calculus is introduced. After studying this fundamental calculus, various type structures are associated with it. In particular, object types, recursive types, subtyping, and dynamic types are taken into consideration. The language that can be built from these premises is similar to languages such as Simula and Modula-3. In the following two parts a move beyond basic type constructions is made by investigating the Self type (the type of self). This topic leads directly into the realm of polymorphism, data abstraction, and type operators.
Standard constructions that type theory provides to model these concepts are reviewed and incorporated into the object calculi. Typing rules for the Self type are given and their correctness is proved, in the context of both calculi and languages. The Self type often occurs only as the type of the results of methods. The authors show that, in this special case, it can be understood through a combination of data abstraction and type recursion, and that method inheritance requires polymorphism.


68N01 General topics in the theory of software
68-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science