Operator Declarations

Let's consider how we might declare the Money class, and in particular how to define multiplication and division by integers for it. We'll assume prices are expressed in whole dollars and cents (feel free to substitute your own national currency here). There's no point in storing the dollars and cents separately; we may as well just store the price in cents.

So, here is how our class starts out:

class Money ^=
abstract
    var amount: nat;

    build{!amount: nat};

interface

    build{dollars: nat, cents: nat}
      pre cents < 100
      ^= Money{100 * dollars + cents};
end;

We will deliberately not make amount publicly readable (hence no redeclaration as an interface function); instead we will provide all the required functionality.

We have declared a constructor that builds a Money object directly from an amount in cents; but since this is declared in the abstract section, it is not accessible outside the class. We have also declared an interface constructor that takes separate values for the dollars and cents. Instead of defining this in the usual way with a postcondition, we have used the "^=" symbol to define the result in terms of our abstract constructor.

Let's now redefine the toString method to make monetary amounts printable:

class Money ^=
abstract
var amount: nat;

build{!amount: nat};

interface

    build{dollars: nat, cents: nat}
      pre cents < 100
      ^= Money{100 * dollars + cents};


       redefine function toString: string


         ^= "$"                              // 
currency indicator


            ++ (amount/100).toString        
// number of dollars 


            ++ "."                          
// separate dollars and cents


            ++ ( let cents ^=
(amount % 100).toString;


                
[#cents = 1]:


                   
cents.prepend(`0`),      // 1 digit so add a leading zero


                
[#cents = 2]:


                   
cents                   
// 2 digits so leave alone


               );

end;

Now let's add a method for adding two amounts of Money together. We could declare a function add for this purpose:

function add(other: Money): Money
^= Money{amount + other.amount};

However, it is much more natural to use the "+" operator to denote addition. We can declare a "+" operator for class Money using the following declaration:

class Money ^=
abstract
var amount: nat;

build{!amount: nat};

interface

    build{dollars: nat, cents: nat}
      pre cents < 100
      ^= Money{100 * dollars + cents};

    redefine function toString: string
      ^= "$"                              // currency indicator
         ++ (amount/100).toString         // number of dollars
         ++ "."                           // separate dollars and cents
         ++ ( let cents ^= (amount % 100).toString;
              [#cents = 1]:
                 cents.prepend(`0`),      // 1 digit so add a leading zero
              [#cents = 2]:
                 cents                    // 2 digits so leave alone
            );


        operator +(other: Money): Money

          ^= Money{amount + other.amount};

end;

Because we have declared a parameter, this is a declaration of a binary "+" operator (we would declare a unary "+" operator by omitting the parameter). When "+" is used between two expressions of type Money, the operator will be invoked with the left-hand operand taking the role of self and the right-hand operand taking the role of other.

Now let's add another operator to the interface section, this time to multiply the current Money object by a nonnegative integer:

operator *(other: nat): Money
^= Money{amount * other};

This operator allows us to write expressions like price * 2, where price is of type Money. But what if we want to allow 2 * price as well? Class int does not include an operator "+" taking a parameter of type Money and no mechanism is provided for adding one. However, we can add an inverted binary operator declaration to class Money like this:

operator (other: nat)*: Money
^= Money{amount * other};

By declaring the parameter before the operator symbol "*" instead of after it, we signify that this operator declaration matches a use of "*" with a left-hand operand of type nat and a right-hand operand of type Money.

All that is left is to add an operator to divide a sum of money by an integer, rounding up:

    operator /(other: nat): Money
      pre other ~= 0
      ^= Money{(amount + other - 1) / other};

Note the precondition to ensure that a sum of money cannot be divided by zero.

Next: Declaring comparison operators