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++
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
but not for
To see why
public inheritance is special,
consider a class
PlusAccount which is derived from a public
A class derived from a public base class is called a subtype.
In our example,
PlusAccount is a subtype of
We also say that
BankAccount is a supertype
In C++ a pointer variable,
ba, of type
can point to either a
or to a
(Similarly, a C++ reference to a
BankAccount can be an alias
What happens when one executes the following C++ code?
Depending on the run-time type of
C++ will execute either
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
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
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]
(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:
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]
(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
public base classes [Dhara-Leavens96].
Larch/C++ does not use specification inheritance
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
If both the
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
However, if either
Derived are the names of
sorts from explicitly-given LSL traits, then
the user must tell Larch/C++ how the abstract values of sort
can be interpreted as abstract values of sort
In either case, there is a mapping defined between the abstract values
Derived in a state and the abstract values of
in that state.
Using this mapping,
the specification of each
virtual member function of
Base can be inherited by class
that is, the specification of each
virtual member function
Base must be satisfied by the corresponding member function
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.