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?
ba->deposit(Money(50.00))
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.