×

Object oriented programming. A unified foundation. (English) Zbl 0871.68024

Progress in Theoretical Computer Science. Basel: Birkhäuser. xviii, 366 p. (1996).
The book provides a model for uniform analysis of the basic issues of object-oriented programming. It is a revised and extended version of the author’s Ph. D. thesis. The book is self contained and may be used by researchers, teachers and practitioners as well. In a short Presentation, the author hints the reader to the most appropriate reading path.
The book contains three parts. The first one, ”Introduction”, has two chapters. Chapter 1 is about the background of \(\lambda\) -calculus. Chapter 2 is a quick overview of the book, made chapter by chapter.
The main part is the second one, containing the chapters 3 to 10. It is named ”Simple Typing” and is devoted to the author’s model of object -oriented programming. Chapter 3, ”Object-oriented programming” , discusses the kernel features of object-oriented programming by means of a mini object- oriented language called ”Kernel Object- Oriented Language” (KOOL). It is a functional language and follows the style of Simula. It includes those features considered by the author as necessary for for a unified foundation of object- oriented programming (classes, methods, overloading, late binding, inheritance, extended classes, type checking). Chapter 4, ”The \(\lambda \&\)-calculus” presents the overloaded- based model. The symbol & is an operator used to glue two functions together in an overloaded one. Thus, the term \(M\&N\) denotes an overloaded function of two branches, \(M\) and \(N\), one of which will be selected according to the type of the argument. Chapter 5, ”Covariance and contravariance: conflict without a cause” clarifies the role of these topics in subtyping. The author uses the introduced model to argue that covariance and contravariance appropriately characterise two distinct and independent mechanisms. They are viewed as non antagonistic concepts, each of them having its own use: covariance for specialisation and contravariance for substituitivity. The chapter ends by three ”golden rules’ that summarise its content: 1. do not use (left) covariance for arrow subtyping; 2. use covariance to override parameters that drive dynamic method selection; 3. when overriding a binary (or \(n\)-ary) method, specify its behaviour not only for the actual class but also for its ancestors. Chapter 6, ”Strong Normalization” studies the normalization properties of \(\lambda\&\). It is shown that \(\lambda\)- calculus is not strongly normalising. It is given a sufficient condition to have strong normalization and are defined two expressive systems that satisfy it. These systems are expressive enough to model object- oriented programming and are used in Chapter 10 to study the mathematical meaning of overloading. Chapter 7 presents three different systems directly issued from \(\lambda\&\): 1. the extension of \(\lambda\&\) by addition of explicit coercions; 2. a modification of \(\lambda\&\) calculus with a new reduction rule; 3. a calculus in which regular functions and overloaded ones are introduced by the same abstraction operator, which therefore unifies them. Chapter 8 is devoted to formal interpretation of KOOL language in the introduced overloading based model. Due to the fact that \(\lambda\&\) is not adequate to a formal study of the properties of object- oriented languages, a new meta language called \(\lambda\)-object is introduced to prove properties of an object-oriented language. The \(\lambda\)-object language enriches the \(\lambda\&\)-calculus by some new features (commands to define new types, to work on their representation, to handle the subtyping hierarchy, to change the type of a term or to modify a discipline of despatching etc.) that are necessary to reproduce the constructs of a programming language and lacking in \(\lambda \&\). Chapter 9, ”Imperative features and other widgets”, presents in a less formal manner some features of practical interest which can be included in KOOL. Thus, this functional language can be upgraded to a realistic object-oriented language adding some imperative commands. It may be also used a unique form of application both for overloaded and regular functions. At last, the type system of KOOL may be modified to implement signatures. Chapter 10, ”Semantics”, goes deeply inside the following problems poses by the semantics of \(\lambda \&\)-calculus: pre-order relation between types; type-dependent computation; late-binding; impredicativity introduced by the definition of subtyping for the overloaded types. It is underlined that some of these issues can not be handled in the \(\lambda \&\)-calculus.
This is a motivation to study in the Part III of the book a second order object- oriented language. This mechanism is base on Girard’ system \(F\), which is enriched to correspond to the implementation of late binding. There are still some features that are not straightforwardly handled, such as super and coerce.
In the last chapter, ”Conclusion”, the author fixes his book in the frame of other related works.

MSC:

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