| Title: | An Imperative, First-Order Calculus with Object Extension |
|---|---|
| Authors: | V. Bono and K. Fisher |
| Published: |
Abstract:
This paper presents an imperative object calculus, designed to support class-based programming via a combination of extensible objects and encapsulation. This calculus simplifies the language presented in Fisher's Thesis in that, like C++ and Java, it chooses to support an imperative semantics instead of method specialization. We show how Java-style classes and ``mixins'' may be coded in this calculus, prove a soundness theorem (via a subject reduction property), and give a sound and complete typing algorithm.
| Title: | On the relationship between classes, objects, and data abstraction |
|---|---|
| Authors: | K. Fisher and J.C. Mitchell |
| Published: | Proceedings of the Internationall Summer School on Mathematics of Program Construction, Marktoberdorf, Germany, Springer LNCS, 1997 (to appear). |
Abstract:
While most object-oriented programming is done in class-based languages, the trend in theoretical study has been to develop formal systems that are object-based, without classes and often without explicit inheritance mechanisms. This paper studies the correspondence between object primitives and class constructs of the form found in C++, Eiffel, and Java. The main qualitative insight is that such classes require both an extensible aggregate, to serve as the basis for inheritance, and a non-extensible form of object to support subtyping. We compare three approaches to modeling classes, the first using records of object components called ``premethods'' and the latter two using an extensible form of object called a ``prototype.'' While the first approach uses fewer primitive operations on objects, it does not provide several important features of class-based languages. In the latter two approaches, we overcome these deficiencies by combining prototypes with standard abstraction mechanisms. All three treatments of classes use translations into provably sound object calculi.
| Title: | A Calculus for Concurrent Objects |
|---|---|
| Authors: | P. DiBlasio and K. Fisher |
| Published: | CONCUR '96: Concurrency Theory, Springer LNCS 1119, 655-670. |
Abstract:
This paper presents an imperative and concurrent extension of the functional object-oriented calculus described in A Lambda Calculus of Objects and Method Specialization. It belongs to the family of so-called prototype-based object-oriented languages, in which objects are created from existing ones via the inheritance primitives of object extension and method override. Concurrency is introduced through the identification of objects and processes. To our knowledge, the resulting calculus is the first concurrent object calculus to be studied. We define an operational semantics for the calculus via a transition relation between configurations, which represent snapshots of the run-time system. Our static analysis includes a type inference system, which statically detects {\it message-not-understood} errors, and an effect system, which guarantees that synchronization code, specified via guards, is side-effect free. We present a subject reduction theorem, modified to account for imperative and concurrent features, and type and effect soundness theorems.
| Title: | Classes = Objects + Data Abstraction |
|---|---|
| Authors: | K. Fisher and J.C. Mitchell |
| Published: | Stanford Technical Note: STAN-CS-TN-96-31 |
Abstract:
We describe a type-theoretic foundation for object systems that include ``interface types'' and ``implementation types,'' in the process accounting for access controls such as C++ private, protected and public levels of visibility. Our approach begins with a basic object calculus that provides a notion of object, method lookup, and object extension (an object-based form of inheritance). In this calculus, the type of an object gives an interface, as a set of methods (public member functions) and their types, but does not imply any implementation properties such as the presence or layout of any hidden internal data. We extend the core object calculus with a higher-order form of data abstraction mechanism that allows us to declare supertypes of an abstract type and a list of methods guaranteed not to be present. This results in a flexible framework for studying and improving practical programming languages where the type of an object gives certain implementation guarantees, such as would be needed to statically determine the offset of a function in a method lookup table or safely implement binary operations without exposing the internal representation of objects. We prove type soundness for the entire language using operational semantics and an analysis of typing derivations. Two insights that are immediate consequences of our analysis are the identification of an anomaly associated with C++ private virtual functions and a principled, type-theoretic explanation (for the first time, as far as we know) of the link between subtyping and inheritance in C++, Eiffel and related languages.
| Title: | A Delegation-Based Object Calculus with Subtyping |
|---|---|
| Authors: | K. Fisher and J.C. Mitchell |
| Published: | Fundamentals of Computation Theory (FCT'95), Springer LNCS 965, 1995, 42-61. |
Abstract:
This paper presents an untyped object calculus that reflects the capabilities of so-called delegation-based object-oriented languages. A type inference system allows static detection of errors, such as message not understood, while at the same time allowing the type of an inherited method to be specialized to the type of the inheriting object. The main advance over previous work is the provision for subtyping in the presence of delegation primatives. This is achieved by distinguishing a prototype, whose methods may be extended or replaced, from an object, which only responds to messages for which it already has methods. An advantage of this approach is that we have full subtyping without restricting the ``run-time'' use of inheritance. Type soundness is proved using operational semantics and an analysis of typing derivations.
| Title: | A Lambda Calculus of Objects and Method Specialization |
|---|---|
| Authors: | K. Fisher, F. Honsell, and J.C. Mitchell |
| Published: | Nordic J. Computing, 1:3-37, 1994. Preliminary version appeared in Proc. IEEE Symp. on Logic in Computer Science, 1993, 26-38. |
Abstract:
This paper presents an untyped lambda calculus, extended with object primitives that reflect the capabilities of so-called delegation-based object-oriented languages. A type inference system allows static detection of errors, such as message not understood, while at the same time allowing the type of an inherited method to be specialized to the type of the inheriting object. Type soundness is proved using operational semantics and examples illustrating the expressiveness of the pure calculus are presented.
| Title: | The Development of Type Systems for Object-Oriented Languages |
|---|---|
| Authors: | K. Fisher and J.C. Mitchell |
| Published: | Theory and Practice of Object Systems, 1(3):189-220, 1995. This paper is an updated version of "Notes on Typed Object-Oriented Programming," which appeared in Proc. Theoretical Aspects of Computer Software, Springer LNCS 789, 1994, 844-885. This paper also appears as Stanford Technical Note STAN-CS-TN-96-30. |
Abstract:
This paper, which is partly tutorial in nature, summarizes some basic research goals in the study and development of typed object-oriented programming languages. These include both immediate repairs to problems with existing languages and the long-term development of more flexible and expressive, yet type-safe, approaches to program organization and design. The technical part of the paper is a summary and comparison of three object models from the literature. We conclude by discussing approaches to selected research problems, including changes in the type of a method from super class to sub class and the use of types that give information about the implementations as well as the interfaces of objects. Such implementation types seem essential for adequate typing of binary operations on objects, for example.
| Title: | What is an Object-Oriented Programming Language? |
|---|---|
| Authors: | K. Fisher and J.C. Mitchell |
Abstract:
This document is a set of rough notes on basic features of object-oriented programming. It is based on the first section of the paper `` Notes on typed object-oriented programming,'' Proc. Theoretical Aspects of Computer Software, Springer LNCS 789, 1994, pages 844-885. It is used in CS242, Stanford's masters-level programming course to teach the fundamental concepts of object-oriented programming.