// @(#)$Id: MutableMoney2.h,v 1.2 1998/10/05 23:37:59 leavens Exp $
// This version of MutableMoney is the desugared form of MutableMoney.h.

#ifndef MutableMoney_h
#define MutableMoney_h

#include "Money.h"

//@ uses MutableMoneyTrait;
//@ uses NoContainedObjects(MutableMoney);

class MutableMoney : public Money
#include "MutableMoney.bse"
{
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^;
  //@ }

#include "MutableMoney.pri"
};

#endif

[Index]

HTML generated using lcpp2html.