When the abstract values of a class are specified by using a LSL trait, instead of using specification variables, then the semantics of specification inheritance is a bit more complex than that described in the previous section. In this section we describe how to specify derived classes when either the derived class, or one of its public subclasses has a trait given explicitly. We also describe how to specify weak behavioral subtypes.
The key idea is that the user must specify how the abstract values of the derived class can be interpreted, in a given state, as abstract values of each of the relevant public base classes. When the derived class has its abstract values explicitly described by a trait, this must be done for each of its public base classes. When the derived class has its abstract values described by using specification variables, this must only be done for each of the public base classes that have their abstract values explicitly described by a trait.
The user tells Larch/C++ how the abstract values of a derived class can be interpreted as abstract values of a public base class by writing a simulates-clause in the derived class specification. The simulates-clause for a public base class, names a trait function that maps the sort of abstract values for the derived class to the abstract values of that base class. This trait function is called a simulation function (or coercion function [America87] [Liskov-Wing93] [Liskov-Wing93b]).
For simple cases, the signature of the simulation function is
given by the signature of f in the following trait.
% @(#)$Id: SimulationFun.lsl,v 1.1 1995/01/08 00:46:23 leavens Exp $
SimulationFun(f, Derived, Base): trait
introduces
f: Derived -> Base
In the syntax that follows,
the simulation function is named by a fcnId.
By using the keyword weakly,
the user tells Larch/C++ that a weak behavioral subtype is being defined,
instead of a strong behavioral subtype.
(When the simulation function is constructed automatically by Larch/C++,
the by fcnId part of the syntax can be omitted to indicate
a weak behavioral subtype.)
simulates-clause ::= [weakly]simulatessupertype-list;supertype-list ::= supertype [,supertype ] ... supertype ::= sort-name [byfcnId ]
As an example, consider a type MutableMoney
that is derived from the public base class
Money
(see section 7.1.2 A Design with a Nontrivial Trait (Money)).
This example is adapted from Dhara's Ph.D. dissertation [Dhara97],
which used it, as we will here, to explain the idea of
weak behavioral subtyping.
In this example an instance of MutableMoney
will act like a Money object with the same amount of pennies.
However, unlike Money, whose objects are immutable,
MutableMoney will also have mutators.
Hence MutableMoney will only be a weak behavioral subtype
of Money.
This means that a MutableMoney object will only act like a
Money object when manipulated by the member functions of
the type Money, assuming that there is no way to simultaneously
mutate it (e.g., by an alias).
(Exact conditions for on aliasing and how to reason about
programs using weak behavioral subtyping a matter of current research,
see [Dhara97] for details.)
As with the class Money,
we specify the abstract values of MutableMoney explicitly.
This is done in the following trait, by including the trait
Money(MutableMoney for Money).
The trait Money is also included, thus overloading the constructors
such as pennies.
The new operation introduced is toMoney,
which tells how to take a MutableMoney value and coerce it to
a Money value.
(The trait also includes axioms to ensure that the values of the
constants MONEY_MAX and MONEY_MIN are the same for
MutableMoney as they are for Money.)
% @(#)$Id: MutableMoneyTrait.lsl,v 1.3 1997/07/31 02:41:11 leavens Exp $
MutableMoneyTrait: trait
includes MoneyTrait, MoneyTrait(MutableMoney for Money)
introduces
toMoney: MutableMoney -> Money
asserts
\forall p: long
toMoney(MONEY_MAX) == MONEY_MAX:Money;
toMoney(MONEY_MIN) == MONEY_MIN:Money;
toMoney(pennies(p)) == pennies(p);
implies
MutableMoneyHom
The following is the interface specification
of the derived class, MutableMoney.
// @(#)$Id: MutableMoney.lh,v 1.3 1997/07/30 20:03:02 leavens Exp $
#ifndef MutableMoney_lh
#define MutableMoney_lh
#include "Money.lh"
//@ uses MutableMoneyTrait;
//@ uses NoContainedObjects(MutableMoney);
class MutableMoney : public Money {
public:
//@ weakly simulates Money by toMoney;
MutableMoney(double amt) throw();
//@ behavior {
//@ requires inRange(money(rational(amt)));
//@ constructs self;
//@ ensures self' = money(rational(amt));
//@ }
MutableMoney(long int cts = 0L) throw();
//@ behavior {
//@ requires inRange(pennies(cts));
//@ constructs self;
//@ ensures self' = pennies(cts);
//@ }
virtual void AddIn(const Money & m2) throw();
//@ behavior {
//@ requires assigned(m2, pre) /\ inRange(self^ + m2\any);
//@ modifies self;
//@ ensures liberally self' + m2\any;
//@ example liberally self^ = money(300/1) /\ m2\any = money(400/1)
//@ /\ self' = money(700/1);
//@ }
virtual void SubtractIn(const Money & m2) throw();
//@ behavior {
//@ requires assigned(m2, pre) /\ inRange(self^ + m2\any);
//@ modifies self;
//@ ensures liberally self' - m2\any;
//@ example liberally self^ = money(700/1) /\ m2\any = money(400/1)
//@ /\ self' = money(300/1);
//@ }
virtual void MultiplyIn(double factor) throw();
//@ behavior {
//@ requires inRange(rational(factor) * self^);
//@ ensures liberally self' = rational(factor) * self^;
//@ }
};
#endif
Notice the weakly simulates clause in the above specification.
It says that MutableMoney is a weak behavioral subtype
of Money.
It also says
what abstract value each MutableMoney value simulates.
That is, a MutableMoney value mm simulates
the Money value toMoney(mm).
The simulation function should have the property that,
it commutes with all the trait functions
that take the supertype as an argument.
This property is asserted in the following trait,
which is implied by the trait MutableMoney given above.
Technically, this property makes the simulation function a homomorphism
on the abstract values.
Hence the property is called the homomorphism property.
% @(#)$Id: MutableMoneyHom.lsl,v 1.2 1997/07/31 20:59:42 leavens Exp $
MutableMoneyHom: trait
assumes MutableMoneyTrait
asserts
\forall mm, mm1, mm2: MutableMoney, q: Q
dollars(mm) == dollars(toMoney(mm));
cents(mm) == cents(toMoney(mm));
toMoney(money(q)) == money(q);
toMoney(mm1 + mm2) == toMoney(mm1) + toMoney(mm2);
toMoney(mm1 - mm2) == toMoney(mm1) - toMoney(mm2);
toMoney(q * mm) == q * toMoney(mm);
(mm1 > mm2) == toMoney(mm1) > toMoney(mm2);
(mm1 < mm2) == toMoney(mm1) < toMoney(mm2);
(mm1 >= mm2) == toMoney(mm1) >= toMoney(mm2);
(mm1 <= mm2) == toMoney(mm1) <= toMoney(mm2);
inRange(mm) == inRange(toMoney(mm));
One way to view the homomorphism property is that it allows Larch/C++
to define all the trait functions that take abstract values
of the supertype,
making these trait functions applicable to the abstract values of the subtype.
The definitions of such overloaded trait functions would be like those given
in the trait MutableMoneyHom.
Because the trait functions that take abstract values of the supertype can be thought of as defined on the abstract values of the subtype, any specification of a function taking arguments of the supertype can be interpreted in a standard way for arguments of the subtype. Indeed, any specification need only mention one type, and is automatically valid for all subtypes of that type. This property is called modular specification in [Leavens90].
Modular specification at the interface level is achieved by the use of supertype abstraction. In practicing supertype abstraction, the reader of a specification thinks in terms of the abstract values of the types written (statically) in the specification. If subtyping is being used, the reader's view corresponds to using the simulation function to map the abstract values of the subtype up to the type used in the specification.
As in the previous subsection, the ability to interpret the supertype's specifications for abstract values of the subtype means that one can inherit the supertype's specifications. As before, inheritance of specifications can be thought of as including the supertype's specification as additional spec-cases, added to those given for the member function in the subtype. (This does not apply non-virtual function members, including constructors, as these are not inherited. However, it does apply to virtual destructors, which are inherited.) The inclusion of each spec-case from the corresponding trait function of a supertype in the subtype's specification body makes the subtype's function satisfy that supertype's specification. The subtype need not have anything specified for it, in which case the meaning is determined completely by the specifications of its supertypes. If the subtype specification has additional spec-cases, these must be satisfied in addition to those of each supertype. That is, when there are multiple supertypes with the same virtual member function (of the same argument types), then all of the specifications must be satisfied. (Sometimes this may lead to a specification that cannot be implemented.)
The only difference from the previous section, where specification variables were used to define the abstract values instead of explicit traits, is that the specifications of the supertype cannot be literally copied to the subtype, but must use the simulation function to avoid type errors. This difference, is mostly a technical detail, and so if you are not interested in such details, you may want to skim the rest of this subsection lightly.
The basic technical idea is to use the simulation function on each subterm
that would have the subtype's abstract value in the specification
cases, invariants, and history constraints copied from the supertype.
Usually this boils down to, for example,
changing self^ to toMoney(self^),
self' to toMoney(self'),
and self\any to toMoney(self\any).
The other important technical point is that when copying the history
constraint for a weak behavioral subtype, the history constraint is
only applied to the public virtual member functions of the weak
behavioral supertype [Dhara-Leavens96].
For example, since MutableMoney is only a weak behavioral subtype
of Money, the history constraint specified for Money
is not applied to the new member functions AddIn, SubtractIn,
and MultiplyIn. This allows these new member functions to be mutators.
To show this in detail, the following is an equivalent specification of
MutableMoney, which shows the effect of specification inheritance.
Notice in particular the inherited history constraint.
// @(#)$Id: MutableMoney2.lh,v 1.4 1998/08/27 22:42:08 leavens Exp $
#ifndef MutableMoney2_lh
#define MutableMoney2_lh
#include "Money.lh"
//@ uses MutableMoneyTrait;
//@ uses NoContainedObjects(MutableMoney);
class MutableMoney : public Money {
public:
//@ weakly simulates Money by toMoney;
// inherited invariant
//@ invariant inRange(toMoney(self\any));
// inherited constraint
//@ constraint toMoney(self') = toMoney(self^)
//@ for virtual long int Dollars() const throw(),
//@ virtual long int Cents() const throw(),
//@ virtual Money & operator + (const Money & m2) const throw(),
//@ virtual Money & operator - (const Money & m2) const throw(),
//@ virtual Money & operator * (double factor) const throw(),
//@ virtual bool operator == (const Money & m2) const throw(),
//@ virtual bool operator > (const Money & m2) const throw(),
//@ virtual bool operator >= (const Money & m2) const throw(),
//@ virtual bool operator < (const Money & m2) const throw(),
//@ virtual bool operator <= (const Money & m2) const throw();
MutableMoney(double amt) throw();
//@ behavior {
//@ requires inRange(money(rational(amt)));
//@ constructs self;
//@ ensures self' = money(rational(amt));
//@ }
MutableMoney(long int cts = 0L) throw();
//@ behavior {
//@ requires inRange(pennies(cts));
//@ constructs self;
//@ ensures self' = pennies(cts);
//@ }
// inherited virtual member function specifications follow
virtual ~Money() throw();
//@ behavior {
//@ ensures true;
//@ }
//@ spec virtual long int Dollars() const throw();
//@ behavior {
//@ ensures result = dollars(toMoney(self\any));
//@ }
//@ spec virtual long int Cents() const throw();
//@ behavior {
//@ ensures result = cents(toMoney(self\any));
//@ }
//@ spec virtual Money & operator + (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre) /\ inRange(toMoney(self\any) + m2\any);
//@ ensures returns;
//@ also
//@ requires assigned(m2, pre);
//@ ensures liberally fresh(result) /\ assigned(result, post)
//@ /\ toMoney(result') = toMoney(self\any) + m2\any;
//@ example liberally toMoney(self\any) = money(300/1)
//@ /\ m2\any = money(400/1)
//@ /\ toMoney(result') = money(700/1)
//@ /\ fresh(result) /\ assigned(result, post);
//@ }
//@ spec virtual Money & operator - (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre) /\ inRange(toMoney(self\any) - m2\any);
//@ ensures returns;
//@ also
//@ requires assigned(m2, pre);
//@ ensures liberally fresh(result) /\ assigned(result, post)
//@ /\ toMoney(result') = toMoney(self\any) - m2\any;
//@ }
//@ spec virtual Money & operator * (double factor) const throw();
//@ behavior {
//@ requires inRange(rational(factor) * toMoney(self\any));
//@ ensures returns;
//@ also
//@ ensures liberally fresh(result) /\ assigned(result, post)
//@ /\ toMoney(result') = rational(factor) * toMoney(self\any);
//@ }
//@ spec virtual bool operator == (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre);
//@ ensures result = (toMoney(self\any) = toMoney(m2\any));
//@ ensures redundantly result =
//@ (dollars(toMoney(self\any)) = dollars(m2\any)
//@ /\ cents(toMoney(self\any)) = cents(m2\any));
//@ }
//@ spec virtual bool operator > (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre);
//@ ensures result = (toMoney(self\any) > m2\any);
//@ }
//@ spec virtual bool operator >= (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre);
//@ ensures result = (toMoney(self\any) >= m2\any);
//@ }
//@ spec virtual bool operator < (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre);
//@ ensures result = (toMoney(self\any) < m2\any);
//@ }
//@ spec virtual bool operator <= (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre);
//@ ensures result = (toMoney(self\any) <= m2\any);
//@ }
// end of inherited specs
virtual void AddIn(const Money & m2) throw();
//@ behavior {
//@ requires assigned(m2, pre) /\ inRange(self^ + m2\any);
//@ modifies self;
//@ ensures liberally self' + m2\any;
//@ example liberally self^ = money(300/1) /\ m2\any = money(400/1)
//@ /\ self' = money(700/1);
//@ }
virtual void SubtractIn(const Money & m2) throw();
//@ behavior {
//@ requires assigned(m2, pre) /\ inRange(self^ + m2\any);
//@ modifies self;
//@ ensures liberally self' - m2\any;
//@ example liberally self^ = money(700/1) /\ m2\any = money(400/1)
//@ /\ self' = money(300/1);
//@ }
virtual void MultiplyIn(double factor) throw();
//@ behavior {
//@ requires inRange(rational(factor) * self^);
//@ ensures liberally self' = rational(factor) * self^;
//@ }
};
#endif
To summarize, when a specification of a member function of a class Base
is inherited in a class Derived, the sort of self changes
from Obj[Base] to Obj[Derived].
Hence the sort of self^ is Derived,
as is the sort of self'.
To avoid the sort errors that would occur when self^
and self' (and their equivalent forms)
are passed to trait functions that expect an argument of the supertype's sort,
a call to the simulation function is wrapped around such subterms.
(See our papers on this subject [Dhara-Leavens96], for more details.)
Using such a rewriting of specification inheritance allows us to think of specification inheritance as a (very convenient) syntactic sugar.
Go to the first, previous, next, last section, table of contents.