Inheritance of specifications for classes that are written using specification variables involves simply copying the specifications of the virtual member functions from the base class to the derived class. Since the specification variables of the base class are also in the derived class, these specifications automatically have a sensible meaning.
For an example, consider again the types BankAccount
and PlusAccount.
We specify the abstract values of the supertype by using
two specification variables: credit and owner
The credit is a specification variable of type Money,
and owner is a specification variable of an abstract string type.
// @(#)$Id: BankAccount.lh,v 1.17 1997/07/28 21:02:52 leavens Exp $
#ifndef BankAccount_h
#define BankAccount_h
#include "Money.lh"
#include "AbstractString.lh"
class BankAccount {
public:
//@ spec Money credit;
//@ spec String<char> owner;
//@ invariant credit\any >= 0;
//@ constraint owner^ = owner';
BankAccount(Money amt, const char *own) throw();
//@ behavior {
//@ uses cpp_const_char_string;
//@ requires pennies(1) <= amt /\ nullTerminated(own, pre);
//@ modifies credit, owner;
//@ ensures credit' = amt /\ owner' = uptoNull(own, pre);
//@ }
virtual ~BankAccount() throw();
//@ behavior {
//@ ensures true;
//@ }
virtual Money balance() const throw();
//@ behavior {
//@ ensures result = credit\any;
//@ }
virtual void pay_interest(double rate) throw();
//@ behavior {
//@ requires 0.0 <= rate /\ rate <= 1.0;
//@ modifies credit;
//@ ensures credit' = rational(1.0 + rate) * credit^;
//@ example rate = 0.05 /\ credit^ = money(400/1)
//@ /\ credit' = money(420/1);
//@ }
virtual void deposit(Money amt) throw();
//@ behavior {
//@ requires amt >= 0;
//@ modifies credit;
//@ ensures credit' = credit^ + amt;
//@ example credit^ = pennies(40000) /\ amt = pennies(1)
//@ /\ credit' = pennies(40001);
//@ }
virtual void withdraw(Money amt) throw();
//@ behavior {
//@ requires 0 <= amt /\ amt <= credit^;
//@ modifies credit;
//@ ensures credit' = credit^ - amt;
//@ example credit^ = pennies(40001) /\ amt = pennies(40000)
//@ /\ credit' = pennies(1);
//@ }
};
#endif
See section 7.1.2 A Design with a Nontrivial Trait (Money)
for the included interface specification Money.
The type String<char> is specified in the file
`AbstractString.h'
(see section 7.1.1 A First Class Design (Person) for details.
The subtype, PlusAccount, is intended to have objects with
both a savings and a checking account. These objects act like
BankAccount objects with a credit that is the sum of their
savings and checking accounts.
By using specification variables, the owner and credit
members of BankAccount are inherited by PlusAccount.
Hence each PlusAccount object has both of these specification variables,
in addition to the specification variables it declares itself.
As a programmer, your first instinct may be to only add one more
specification variable to PlusAccount, and to reuse the
inherited member, credit for either the savings or checking account
balance. This would be reasonable in a program, as then it would save space,
as instances would only have two Money variables, instead of three.
However, remember that these are just specification variables,
not real variables, and they take up no space in objects at all.
Indeed, it would be inconsistent to treat the credit member
differently than it was treated in BankAccount,
which under this view is the sum of the savings and checking balances.
So in the following specification, we use a common "trick":
the specification has three specification variables of type Money:
the inherited credit, savings, and checking.
We specify that credit depends on savings and checking
and, by using an invariant, that its value is their sum.
The depends-clause allows savings and checking
to be modified whenever credit is mentioned in a modifies-clause.
Note that this does not work the other way around;
for example in the extra case for pay_interest below,
just mentioning checking in the modifies clause is incorrect,
as it would say that credit could not be changed.
The represents-clause says how savings and checking
together represent credit.
// @(#)$Id: PlusAccount.lh,v 1.21 1999/03/04 03:37:08 leavens Exp $
#ifndef PlusAccount_lh
#define PlusAccount_lh
#include "BankAccount.lh"
class PlusAccount : public BankAccount {
public:
//@ spec Money savings;
//@ spec Money checking;
//@ depends credit on savings, checking;
//@ represents credit by credit\any = savings\any + checking\any;
//@ invariant savings\any >= 0 /\ checking\any >= 0;
// the constraint is inherited
//@ constraint checking^ = checking'
//@ for void deposit(Money amt);
PlusAccount(Money savings_balance, Money checking_balance,
const char * name) throw();
//@ behavior {
//@ uses cpp_const_char_string;
//@ requires pennies(0) < savings_balance
//@ /\ pennies(0) <= checking_balance
//@ /\ nullTerminated(name, pre);
//@ modifies credit, savings, checking, owner;
//@ ensures savings' = savings_balance
//@ /\ checking' = checking_balance
//@ /\ owner' = uptoNull(name, pre);
//@ ensures redundantly credit' = savings' + checking';
//@ }
virtual ~PlusAccount() throw();
//@ behavior {
//@ ensures true;
//@ }
virtual Money balance() const throw();
// balance spec inherited, but it might be reimplemented
virtual void pay_interest(double rate) throw();
//@ behavior {
//@ requires 0.0 <= rate /\ rate <= 1.0;
//@ modifies credit, checking;
//@ ensures checking' = rational(1.0 + rate) * checking^;
//@ example checking^ = money(50000/100) /\ rate = 0.05
//@ /\ checking' = money(52500/100);
//@ // by inheritance, interest also added to savings
//@ }
// withdrawal takes money out of savings first, then checking
virtual void withdraw(Money amt) throw();
//@ behavior {
//@ requires 0 <= amt;
//@ {
//@ requires amt <= savings^;
//@ modifies credit, savings;
//@ ensures unchanged(checking);
//@ // by inheritance, amt is taken out of savings
//@ example savings^ = pennies(40001) /\ amt = pennies(1)
//@ /\ savings^ = pennies(40000)
//@ /\ checking' = checking^;
//@ also
//@ requires savings^ < amt /\ amt <= (savings^ + checking^);
//@ modifies credit, savings, checking;
//@ ensures savings' = pennies(0)
//@ /\ checking' = checking^ - (amt - savings^);
//@ example savings^ = pennies(40000) /\ amt = pennies(52500)
//@ /\ checking^ = pennies(60000)
//@ /\ savings' = pennies(0)
//@ /\ checking' = pennies(47500);
//@ }
//@ }
virtual void checking_deposit(Money amt) throw();
//@ behavior {
//@ requires amt >= 0;
//@ modifies credit, checking;
//@ ensures checking' = checking^ + amt /\ unchanged(savings);
//@ }
// pay_check takes money out of checking first, takes from savings if needed
virtual void pay_check(Money amt) throw();
//@ behavior {
//@ requires 0 <= amt;
//@ {
//@ requires checking^ >= amt;
//@ modifies credit, checking;
//@ ensures checking' = checking^ - amt /\ unchanged(savings);
//@ example checking^ = pennies(52501) /\ amt = pennies(1)
//@ /\ checking' = pennies(52500) /\ unchanged(savings);
//@ also
//@ requires checking^ < amt /\ amt <= (savings^ + checking^);
//@ modifies credit, checking, savings;
//@ ensures savings' = savings^ - (amt - checking^)
//@ /\ checking' = 0;
//@ example savings^ = pennies(52500) /\ checking^ = pennies(40000)
//@ /\ amt = pennies(62500)
//@ /\ savings' = pennies(40000) /\ checking' = pennies(0);
//@ }
//@ }
};
#endif
The interface specification of the subtype PlusAccount
inherits the specification of balance without
respecification.
So what should happen when balance is invoked on
a PlusAccount?
By specification inheritance, it must satisfy
the specification of balance given for BankAccount.
In this kind of example, one can visualize this idea
by copying the specification given for BankAccount to the specification
of PlusAccount.
Hence balance must return the value of credit,
which, by the invariant, is the total of the savings and checking accounts.
Applying specification inheritance to a virtual member function that
is given its own specification is only a bit more complex.
The idea is that the derived class's operation must satisfy both
specifications: the one specified for the base class and the one
specified for the derived class (and both invariants and history constraints).
A good way to visualize this is to consider both specifications
as spec-cases of a single specification.
For example, for pay_interest, the specification for PlusAccount
above gives one spec-case, and the other is given in
the specification for BankAccount.
The expanded form of this specification would look like the following.
// @(#)$Id: PlusAccount_pi.lh,v 1.1 1997/07/31 02:45:09 leavens Exp $
#include "PlusAccount.lh"
extern void PlusAccount::pay_interest(double rate) throw();
//@ behavior {
//@ requires 0.0 <= rate /\ rate <= 1.0;
//@ modifies credit;
//@ ensures credit' = rational(1.0 + rate) * credit^;
//@ example rate = 0.05 /\ credit^ = money(400/1)
//@ /\ credit' = money(420/1);
//@ also
//@ requires 0.0 <= rate /\ rate <= 1.0;
//@ modifies credit, checking;
//@ ensures checking' = rational(1.0 + rate) * checking^;
//@ example checking^ = money(50000/100) /\ rate = 0.05
//@ /\ checking' = money(52500/100);
//@ }
Thus, in the specification of PlusAccount,
it suffices to only say what happens to checking;
what happens to savings can be inferred from
the invariant and the specification given in BankAccount.
Working this out, one sees that interest must be paid on
both the savings and checking parts, as shown by the desugaring above.
Thus the additional spec-case in PlusAccount
keeps an implementation from transferring money
between savings and checking when paying interest.
(See section 6.10 Case Analysis for the meaning of multiple specification cases.)
For deposit, the history constraint added
in PlusAccount says that checking does not change.
Putting this together with the specification given in BankAccount
and the invariant, which says the credit is the sum of
the savings and checking in any state,
this means that the deposit goes entirely into savings.
The member function withdraw has an even more interesting specification;
it inherits a case from BankAccount, and adds two more cases.
The invariant-clauses of public superclasses are also inherited
and must be satisfied by the subclass.
For example, PlusAccount must satisfy the invariant
of BankAccount as well as its own invariant.
In this example, one can visualize the inheritance of the invariant
by copying it to the specification of the subtype.
Except for weak behavioral subtypes (see below), inheritance of history constraints is done in exactly the same way as for invariants. So for such specifications, the subtype must satisfy the history constraints of its supertypes and whatever history constraints are written in its specification.
Go to the first, previous, next, last section, table of contents.