Go to the first, previous, next, last section, table of contents.


7.1.2 A Design with a Nontrivial Trait (Money)

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.