// @(#)$Id: PlusAccount2.lh,v 1.17 1999/03/02 17:56:25 leavens Exp $
// This version of PlusAccount is the desugared form of PlusAccount.h.

#ifndef PlusAccount_h
#define PlusAccount_h

#include "BankAccount.h"

class PlusAccount : public BankAccount
#include "PlusAccount.bse"
{
 public:
  //@ spec Money savings;
  //@ spec Money checking;
  //  This also inherits: spec Money credit and spec String<char> owner

  //@ depends credit on savings, checking;
  //@ represents credit by credit\any = savings\any + checking\any;

  // inherited invariant
  //@ invariant credit\any >= 0;

  //@ invariant savings\any >= 0 /\ checking\any >= 0;

  // inherited constraint
  //@ constraint owner^ = owner';

  //@ constraint checking^ = checking' for void deposit(int cts);

  PlusAccount(Money savings_balance, Money checking_balance,
              const char * name) throw();
  virtual ~PlusAccount() throw();
  virtual Money balance() const throw();
  virtual 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 is the desugared specification of PlusAccount.
// This takes into account both the effects of specification
// inheritance, and the effect of the depends clause above.

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 virtual Money PlusAccount::balance() const throw();
  //@ behavior {  // inherited
  //@    ensures result = credit\any;
  //@ }

extern void PlusAccount::pay_interest(double rate) throw();
  //@ behavior {
  //@    requires 0.0 <= rate /\ rate <= 1.0;
  //@    modifies credit;
  //@    ensures credit' = rational(1.0 + rate) * credit^;
  //@    example rate = 0.05 /\ credit^ = money(400/1)
  //@                        /\ credit' = money(420/1);
  //@  also
  //@    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);
  //@ }

extern void PlusAccount::deposit(Money amt) throw();
  //@ behavior {
  //@    requires amt >= 0;
  //@    modifies credit, savings;  // savings added by the dependency
  //@    ensures credit' = credit^ + amt;
  //@    ensures redundantly checking' = checking^; // by constraint
  //@    ensures redundantly savings' = savings^ + amt; // by invariant
  //@    example credit^ = pennies(40000) /\ amt = pennies(1)
  //@         /\ credit' = pennies(40001);
  //@  }

void PlusAccount::withdraw(Money amt) throw();
  //@ behavior {
  //@    requires 0 <= amt /\ amt <= credit^;
  //@    modifies credit, savings;   // savings added by the dependency
  //@    ensures credit' = credit^ - amt;
  //@    example credit^ = pennies(40001) /\ amt = pennies(40000)
  //@         /\ credit' = pennies(1);
  //@   also
  //@    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.