// @(#)$Id: PlusAccount.h,v 1.18 1999/04/11 15:57:35 leavens Exp $

#ifndef PlusAccount_h
#define PlusAccount_h

#include "BankAccount.h"

class PlusAccount : public BankAccount
#include "PlusAccount.bse"
{
 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( int cts);

  PlusAccount(Money savings_balance, Money checking_balance,
              const char * name) throw();
  ~PlusAccount() throw();
  virtual Money balance() const throw();
  void pay_interest(double rate) throw();
  virtual void withdraw(Money amt) throw();
  virtual void checking_deposit(Money amt) throw();
  virtual void pay_check(Money amt) throw();
#include "PlusAccount.pri"
};

// The following specification of PlusAccount is written using
// specification inheritance.  Note that balance is not respecified here,
// even though it is reimplemented in the code.
// For the rest of the member functions, the only thing said is how
// the checking account is affected.
// Since all these specifications are added (as in case analysis, see
// the manual) to the specifications of the same operations for BankAccount,
// this gives a specification equivalent (semantically) to that
// in the file PlusAccount2.lh.

//@ extern PlusAccount::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';
//@   }

//@ extern PlusAccount::~PlusAccount() throw();
//@   behavior {
//@      ensures true;
//@   }

//@ extern void PlusAccount::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
//@   }

//@ void PlusAccount::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);
//@      }
//@    }

//@ void PlusAccount::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
//@ void PlusAccount::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

[Index]

HTML generated using lcpp2html.