// @(#)$Id: BankAccount.pri,v 1.5 1997/07/24 21:49:12 leavens Exp $
// Private members of BankAccount

private:
  Money * bal;
  const char * ownr;

  //@ invariant assigned(bal, any) /\ nullTerminated(ownr, any);
  //@ depends credit on *(bal\any);
  //@ depends owner on objectsToNull(ownr, any);
  //@ invariant credit\any = (*(bal\any))\any
  //@        /\ owner\any = uptoNull(ownr, any);