For another example, consider the specification
of a class Money.
Although one could also use specification variables
to specify Money, doing so would be inconvenient for clients of
the specification.
The inconvenience arises because Money
does not have easily remembered "parts" and because it is likely
to only have one "part."
This is often the case for types,
like Money whose object cannot be mutated,
and hence are immutable.
For such types, it is better to specify their abstract values
explicitly, using a LSL trait, instead of using specification variables.
This allows clients of the specification to use the abstract values
directly, instead of having to remember the name of a data member.
It also makes Money act more like a C++ built-in type.
It is usually a good idea to look in Guttag and Horning's LSL Handbook (Appendix A of [Guttag-Horning93]) to see if something like what you want has already been specified in LSL. Since there is no trait in Guttag and Horning's LSL handbook for money, we will also specify our own trait.
To define the trait specifying the abstract values of Money,
we begin by asking a question. What information is contained in money?
In the USA, one might immediately think of a number of dollars
and cents, making one think that Money should be modeled
as a tuple of dollars and cents.
However, if one uses such a trait, one quickly finds that
adding and subtracting amounts of money are difficult.
After thinking about this, it may occur to you that a better
model of (US) money is a number of cents.
What trait functions need to be specified?
One can follow the same general idea for specifying a Larch/C++ class,
except that as there is no mutation or destruction in the mathematical
world of LSL, one only needs constructors and observers.
In the following trait there are two constructors:
pennies, which takes a number of pennies and returns
an amount of money, and money, which takes a rational
and converts it into money by rounding down to the nearest cent.
For observers, we will use dollars and cents,
which extract the number of dollars and cents from a given amount
of money. We call the trait that models this basic idea of money
MoneyBasics, and put it in the file `MoneyBasics.lsl'.
% @(#)$Id: MoneyBasics.lsl,v 1.1 1997/07/30 04:54:58 leavens Exp $
MoneyBasics: trait
includes long, Floor(long for int)
introduces
money: Q -> Money
pennies: long -> Money
dollars, cents: Money -> long
asserts
Money generated by pennies
Money partitioned by dollars, cents
\forall q: Q, p: long
money(q) == pennies(floor(q*(100/1)));
dollars(pennies(p)) == div(p, 100);
cents(pennies(p)) == mod(p, 100);
implies
Money generated by money
\forall m: Money
dollars(money(1:Q)) == 1;
cents(money(1:Q)) == 0;
pennies((100*dollars(m)) + cents(m)) == m;
converts
money: Q -> Money,
dollars: Money -> long,
cents: Money -> long
In the asserts section of the trait,
one often writes that the sort is generated by
a subset of the primitive constructors
that are sufficient to make all the values of the type.
In this case, Money is generated by the trait function
pennies.
One also often writes that the sort is partitioned by
a subset of the observers
that are sufficient to distinguish any two values that
should be distinguished.
In this case, Money is partitioned by the trait function
dollars and cents.
What equations to write?
One generally should write an equation telling what trait function
in the partitioned by list (or lacking such a list, each observer)
returns for each primitive constructor
(see [Guttag-Horning78] and page 54 of [Guttag-Horning93]).
In writing the equations it helps to think of functional programming. (Sometimes, although not illustrated by this example, it helps to think of induction with the constructors that do not take arguments of the sort being specified as the base case, and other constructors as inductive cases.)
You might also want to write some implications in the trait.
These are written following the keyword implies,
and can either highlight properties that follow from the axioms,
or can state "obvious" properties
that are used to debug the specification
(as in chapter 7 of [Guttag-Horning93]).
In the trait MoneyBasics the first implication says that
Money is generated by the constructor money.
When one has a second way to specify a property,
such as a way to generate Money, it is often useful to place that
in an implication.
The second and third implications, i.e., the first two implied equations,
are intended to be obvious properties that are true of one dollar.
The last implied equation says how to put dollars and cents back together.
The converts section says that the trait functions money,
dollars, and cents are well-defined relative to the other
trait functions (i.e., pennies).
In the trait MoneyTrait below,
we add to the basic theory some trait functions
to allow money to be added and subtracted, compared,
and checked for being in a certain range.
For interest calculations, we also specify
how to multiply a rational number and an amount of money.
When writing equations for the non-primitive constructors,
one can specify them by stating what observers
do when these functions are applied to combinations of primitive observers.
But often it is convenient to
define them as abbreviations that rewrite into the more primitive trait
functions, which is what is done in the trait for +, -,
and *.
% @(#)$Id: MoneyTrait.lsl,v 1.9 1997/07/30 04:54:59 leavens Exp $
MoneyTrait: trait
includes MoneyBasics, DerivedOrders(Money)
introduces
__+__, __-__: Money, Money -> Money
__*__: Q, Money -> Money
__>__: Money, Money -> Bool
MONEY_MAX, MONEY_MIN: -> Money
inRange: Money -> Bool
asserts
\forall q: Q, p,p1,p2: long, m: Money
pennies(p1) + pennies(p2) == pennies(p1 + p2);
pennies(p1) - pennies(p2) == pennies(p1 - p2);
q * pennies(p1) == pennies(floor(q * (p1/100)));
pennies(p1) > pennies(p2) == p1 > p2;
pennies(10000) < MONEY_MAX;
MONEY_MIN < pennies(-10000);
inRange(m) == MONEY_MIN <= m /\ m <= MONEY_MAX;
implies
TotalOrder(Money)
\forall q,q1,q2: Q, p,p1,p2: long, m,m1,m2: Money
pennies(100*dollars(m)) + pennies(cents(m)) == m;
m1 > m2 == dollars(m1) > dollars(m2)
\/ (dollars(m1) = dollars(m2)
/\ cents(m1) > cents(m2));
converts
__+__: Money, Money -> Money,
__-__: Money, Money -> Money,
__*__: Q, Money -> Money,
__>__: Money, Money -> Bool
You may find, as we did, that you have to go back and add trait functions
to your trait
when they are needed to specify some of the member functions of the class.
For example, we needed to add trait functions to specify an ordering
on money values.
Later we also realized that the LSL Handbook in [Guttag-Horning93]
does not have a trait function floor, which is needed.
This could have been put in the trait, but it seems to be a generally
useful concept, so we made another trait for it.
That trait is given below.
% @(#)$Id: Floor.lsl,v 1.1 1995/11/13 23:31:09 leavens Exp $
Floor(int): trait
includes Rational(int for Int)
introduces
floor: Q -> int
asserts
\forall q: Q
(q-1) < (floor(q)/1);
(floor(q)/1) <= q;
implies
\forall n: int, a,b: P
floor(n/1) == n;
floor(floor(n/a)/b) == floor(n/(a*b));
Even later, we realized that, in order to allow for finiteness
of the representation of money, we had to add the constants
MONEY_MIN and MONEY_MAX to the trait,
and the trait function inRange.
It would be a mistake (contradictory)
to try to enforce these limits in the trait
by adding an assertion of the following form to the trait.
The correct place to do that is in the invariant of the class.
Thus the following would be wrong in the trait.
\forall m: Money inRange(m); % error! contradictory in the trait!
Having written the trait for money,
we can now design and specify the class Money.
Since this is an immutable type, there are no mutator operations.
For constructors, C++ has decided what they can be named.
So we distinguish the constructors on the basis of their argument type.
We use a constructor with a double precision floating point argument,
and one with a number of pennies as an argument.
For observers, we specify functions Dollars and Cents.
We then specify addition, subtraction, interest multiplication,
and various comparison functions.
Thinking about addition and subtraction makes one think
about overflow. To keep things fairly simple in this design,
liberal specification is used to avoid exceptions
(see section 6.12 Liberal Specifications).
The next section has an example with exceptions
(see section 7.1.3 A Class with Exceptions (Stack)).
The design of Money resembles its used trait
because the type is immutable.
// @(#)$Id: Money.lh,v 1.17 1998/08/27 22:42:07 leavens Exp $
#ifndef Money_lh
#define Money_lh
//@ uses MoneyTrait;
//@ uses NoContainedObjects(Money);
class Money {
public:
//@ invariant inRange(self\any);
//@ constraint self' = self^; // Money is immutable
Money(double amt) throw();
//@ behavior {
//@ requires inRange(money(rational(amt)));
//@ constructs self;
//@ ensures self' = money(rational(amt));
//@ }
virtual ~Money() throw();
//@ behavior {
//@ ensures true;
//@ }
Money(long int cts = 0L) throw();
//@ behavior {
//@ requires inRange(pennies(cts));
//@ constructs self;
//@ ensures self' = pennies(cts);
//@ }
virtual long int Dollars() const throw();
//@ behavior {
//@ ensures result = dollars(self\any);
//@ }
virtual long int Cents() const throw();
//@ behavior {
//@ ensures result = cents(self\any);
//@ }
virtual Money & operator + (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre) /\ inRange(self\any + m2\any);
//@ ensures returns;
//@ also
//@ requires assigned(m2, pre);
//@ ensures liberally fresh(result) /\ assigned(result, post)
//@ /\ result' = self\any + m2\any;
//@ example liberally self\any = money(300/1) /\ m2\any = money(400/1)
//@ /\ result' = money(700/1)
//@ /\ fresh(result) /\ assigned(result, post);
//@ }
virtual Money & operator - (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre) /\ inRange(self\any - m2\any);
//@ ensures returns;
//@ also
//@ requires assigned(m2, pre);
//@ ensures liberally fresh(result) /\ assigned(result, post)
//@ /\ result' = self\any - m2\any;
//@ }
virtual Money & operator * (double factor) const throw();
//@ behavior {
//@ requires inRange(rational(factor) * self\any);
//@ ensures returns;
//@ also
//@ ensures liberally fresh(result) /\ assigned(result, post)
//@ /\ result' = rational(factor) * self\any;
//@ }
virtual bool operator == (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre);
//@ ensures result = (self\any = m2\any);
//@ ensures redundantly result = (dollars(self\any) = dollars(m2\any)
//@ /\ cents(self\any) = cents(m2\any));
//@ }
virtual bool operator > (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre);
//@ ensures result = (self\any > m2\any);
//@ }
virtual bool operator >= (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre);
//@ ensures result = (self\any >= m2\any);
//@ }
virtual bool operator < (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre);
//@ ensures result = (self\any < m2\any);
//@ }
virtual bool operator <= (const Money & m2) const throw();
//@ behavior {
//@ requires assigned(m2, pre);
//@ ensures result = (self\any <= m2\any);
//@ }
};
#endif
The first uses-clause in Money says that the trait
MoneyTrait is to be used.
The identity of the name Money in this trait
and the name of the class Money tells Larch/C++ that
it should not automatically construct a trait for Money's abstract values,
but that the abstract values are given explicitly.
The use of the trait NoContainedObjects(Money)
tells Larch/C++ that the abstract values of Money objects
do not contain subobjects.
A definition of the contained_objects trait function is
needed for each sort of abstract value
(see section 7.5 Contained Objects).
When the abstract values are defined explicitly by the user,
then the contained_objects trait function must also be defined.
The most convenient way to do this
when the abstract values contain no subobjects,
is as shown here.
The money abstract values specified in MoneyTrait
may be of any size, but the implementation will have to
impose some limit.
This is the reason for the invariant.
In the invariant, the Larch/C++ keyword self denotes
an arbitrary, assigned, object of type Money.
Its sort, as an object, is Obj[Money].
This is the sort of self throughout this class specification.
The sort of self\any is thus Money,
which is the sort of values specified in the LSL trait MoneyTrait.
Money objects are immutable. For example addition of money
produces a new money object. The history constraint says that,
once a money object is created, its abstract value does not change.
In a history constraint, as in the invariant, self denotes
an arbitrary, assigned, object of type Money.
In the rest of the specification, the keyword self refers
to the object *(this\any); i.e., it refers to the implicit
receiver of a member function call or to the implicit object being constructed
by a constructor.
The second constructor for Money specifies a default for its parameter.
For example, the abstract value of Money(3L) is pennies(3),
and the abstract value of Money() is pennies(0).
The specification of the member function + uses two cases,
separated by the keyword also.
The first case says that the function has to terminate
when the sum is in range.
The second says that if it terminates, it must do the right thing.
(See section 6.10 Case Analysis for details on having multiple spec-cases
in a function specification.
See section 6.12 Liberal Specifications for details on the use of liberally.)
The specification of the member function + uses the trait
function of the same name.
This is not a difficulty for Larch/C++, as the meaning is clear
because the C++ member function cannot be called in a predicate
(see section 4.6 Identifiers for worlds in which identifiers live).
If you think the people reading your specification will
find this kind of thing confusing, you can make things clearer for them
by using different names for each.
Another way to clear up such a potential confusion is to give
an example, as is done in the specification of +
(see section 6.9.1 Examples in Function Specifications).
Because Dollars and the other functions do not modify self,
they refer to the abstract value of self using self\any.
This is a way of saying "either \pre or \post,
it doesn't matter"
(see section 6.2.1 State Functions for details).
A C++ idiom is to take instances as reference parameters to avoid
the run-time overhead of passing them by value.
This is done in the overloadings of the C++ operators +, -,
and so on.
Also these overloaded operators return a reference to a freshly
allocated Money object (see section 6.3.1 Fresh).
In the specification of operator ==,
it should be noted that the C++ type bool
is modeled by the sort Bool.
(See section 11.4 bool for details.)
Go to the first, previous, next, last section, table of contents.