// @(#)$Id: BankAccount.h,v 1.12 1997/07/24 21:00:52 leavens Exp $

#ifndef BankAccount_h
#define BankAccount_h

#include "Money.h"
#include "AbstractString.lh"

class BankAccount
#include "BankAccount.bse"
{
public:
  //@ spec Money credit;
  //@ spec String<char> owner;

  //@ invariant credit\any >= 0;
  //@ constraint owner^ = owner';

  BankAccount(Money amt, const char *own) throw();
  //@ behavior {
  //@    uses cpp_const_char_string;
  //@    requires pennies(1) <= amt /\ nullTerminated(own, pre);
  //@    modifies credit, owner;
  //@    ensures credit' = amt /\ owner' = uptoNull(own, pre);
  //@ }

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

  virtual Money balance() const throw();
  //@ behavior {
  //@    ensures result = credit\any;
  //@ }

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

  virtual void deposit(Money amt) throw();
  //@ behavior {
  //@    requires amt >= 0;
  //@    modifies credit;
  //@    ensures credit' = credit^ + amt;
  //@    example credit^ = pennies(40000) /\ amt = pennies(1)
  //@         /\ credit' = pennies(40001);
  //@  }

  virtual void withdraw(Money amt) throw();
  //@ behavior {
  //@    requires 0 <= amt /\ amt <= credit^;
  //@    modifies credit;
  //@    ensures credit' = credit^ - amt;
  //@    example credit^ = pennies(40001) /\ amt = pennies(40000)
  //@         /\ credit' = pennies(1);
  //@  }
#include "BankAccount.pri"
};

#endif

[Index]

HTML generated using lcpp2html.