Go to the first, previous, next, last section, table of contents.

7.9 Inheritance of Specifications and Subtyping

As in C++, a derived class inherits members of its base classes, and can access the public and protected members it inherits. This is also true of the interface information in a Larch/C++ class specification. In C++, the behavior of the base classes is also inherited to some extent, because the code for virtual member functions in base classes is inherited. However, because one can override definitions of member functions in derived classes, there is no guarantee that the objects of a derived class have any behavioral relationship to objects of its base classes. This is perfectly acceptable for protected and private inheritance, but not for public inheritance.

To see why public inheritance is special, consider a class PlusAccount which is derived from a public base class BankAccount. A class derived from a public base class is called a subtype. In our example, PlusAccount is a subtype of BankAccount. We also say that BankAccount is a supertype of PlusAccount.

In C++ a pointer variable, ba, of type BankAccount * can point to either a BankAccount object, or to a PlusAccount object. (Similarly, a C++ reference to a BankAccount can be an alias for a PlusAccount.) What happens when one executes the following C++ code?


Depending on the run-time type of *ba, C++ will execute either BankAccount::deposit or PlusAccount::deposit. This dynamic binding of a member function to a call can be thought of as a kind of overloading that is resolved at run-time. It allows C++ programs to be polymorphic, and is one of the main features of object-oriented programming.

However, the use of dynamic binding can make reasoning about programs difficult [Leavens-Weihl90] [Leavens91] [Leavens-Weihl95]. In thinking about what ba->deposit(Money(50.00)) does, one should not have to do a case analysis for each subtype. Instead, one would like to reason about what this means using the static type of ba, as would be done if there were no subtypes. This is the idea of supertype abstraction, which means letting supertypes stand for all of their subtypes in reasoning. The advantage of using supertype abstraction in reasoning is that such reasoning does not have to change when new subtypes are added to the program. That is, such reasoning is modular [Leavens-Weihl90] [Leavens91] [Leavens-Weihl95]. (This is important, because one of the things typically done in object-oriented programs is to add in new subtypes of existing types.)

However, supertype abstraction is only valid as a reasoning technique if certain semantic conditions are placed on the behavior of the subtype. A subtype that satisfies such conditions is called a behavioral subtype. The exact conditions that are needed for behavioral subtyping are still a matter of research, but sufficient conditions are already clear: for each virtual member function of each supertype, the subtype's member function (with the same name and argument types) must satisfy the specification of the supertype's member function [America87] [Meyer88] [Liskov-Wing93] [Liskov-Wing93b] [Leino95] [Dhara-Leavens96] [Dhara97]. (There are also various restrictions on types and accessibility, but these are already enforced by C++.)

To support supertype abstraction, a derived class specification in Larch/C++ inherits specifications from its public base classes. This is done in such a way as to force the derived type to be a behavioral subtype of its public base classes [Dhara-Leavens96]. Larch/C++ does not use specification inheritance for protected and private base classes, which allows users to specify derived classes that are not behavioral subtypes (of non-public base classes).

The way specification inheritance works in Larch/C++ is as follows. Consider a class specification Derived. If both the Base and Derived have an implicitly-defined trait (that is, if they both use specification variables), then the abstract values of the sort Base are obtained from the abstract values of Derived by simply omitting the specification variable members not found in Base. However, if either Base or Derived are the names of sorts from explicitly-given LSL traits, then the user must tell Larch/C++ how the abstract values of sort Derived can be interpreted as abstract values of sort Base. In either case, there is a mapping defined between the abstract values of Derived in a state and the abstract values of Base in that state. Using this mapping, the specification of each virtual member function of class Base can be inherited by class Derived; that is, the specification of each virtual member function of class Base must be satisfied by the corresponding member function of class Derived.

We first describe the more usual case, where the specifications of all classes involved are written using specification variables. Then we describe the case where explicitly-given LSL traits are used for some of the classes. Following that, we describe some more details and briefly discuss related work.

Go to the first, previous, next, last section, table of contents.