// @(#)$Id: PlusAccount.lh,v 1.21 1999/03/04 03:37:08 leavens Exp $

#ifndef PlusAccount_lh
#define PlusAccount_lh

#include "BankAccount.lh"

class PlusAccount : public BankAccount {
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(Money amt);

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

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

  virtual Money balance() const throw();
  // balance spec inherited, but it might be reimplemented

  virtual void 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
  //@ }

  // withdrawal takes money out of savings first, then checking
  virtual void 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);
  //@    }
  //@  }

  virtual void 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
  virtual void 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.